nodogoto
Joined 4 years ago
Joined 4 years ago
I bet that what you describe could be implemented with stashes and scripts run on hooks, but that feels like fighting the tool too much. There's probably something we're missing?
Humans aren't capable of doing this, but still make useful drug discoveries. AI can be empowered to conduct research in the real world, it doesn't need to simulate everything.
It's like saying you have an "empty cup of water".
Look up Coq, Agda, Lean, and Idris. I would start with Coq, it's the most used. Idris is more like Haskell and programmer-oriented.
Edit: Nevermind, apparently they were just talking about Haskell...
If the average assignment grades are very high the professor will be inclined to make the assignments more challenging. Cheating disrupts the professor's ability to accurately determine how well their students are grasping the material and adjust accordingly.
For whom is that a goal? Are there really that many individuals at the intersection of "I need to use a theorem prover" and "I don't have formal mathematical training"?