New answers tagged


Look at Agda [1][2] I think that it's exactly what you are looking for. I recommend using its emacs mode for autocompletion and hole/interactive programming. [2]/quick-guide.html A very good introduction is plfa [3], also [2]/tutorial-list.html [1] [2]


You do not have to prove things by induction. For example, you can prove $\forall n : \mathbb{N} \,.\, n = n$ without induction by applying reflexivity. In your proof, we use induction on $a$, but then we do not need to use induction on $b$ and $c$ because we can finish the proof simply using other methods. We could have used induction on $b$ and $c$, and ...


You are conflating two possible meanings of the phrase "mathematics can be automated": "any theorem can be proved true or false by an algorithm" "the practical activity of proving theorems, as presently performed by humans, can instead be performed by computers in an economically-viable fashion" Due to the halting problem, it is impossible for any ...


The notion of automating mathematics is a vague one, and that's accounting for the discrepancy here. One interpretation would be: to automate mathematics would be to produce a machine $M$ which could tell whether or not a given sentence is true (or, more weakly, provable from some agreed-upon set of axioms like $\mathsf{ZFC}$). Even the weaker version is ...


I think this question should give you the answer. In short, if P=NP then any conjecture with a reasonable length proof can be proved by a computer.

Top 50 recent answers are included