4 ms·
Mathematics is the most creative work there is, so if you can automate the tedious work, it helps, but no miracles. Theorem proving requires unnecessarily form
by Nokinside 4y ago
Mathematics is the most creative work there is, so if you can automate the tedious work, it helps, but no miracles. Theorem proving requires unnecessarily formal reasoning chain that is usually more work than worth.
The way most mathematicians work is: First they figure out what the lemma or theorem they want is. Then they try to prove it.
I think theorem proofing will be beneficial for programmers and inside a compiler. Messy program with assertions -> proof -> verified program.
- practal 4y agoI am pretty sure that in 20 years every mathematician will happily use an ITP system. That is because formal reasoning is not unnecessary, but just too burdensome to be done on paper. Ideally a future ITP system will give you the formalisation almost for free, and lets you concentrate on your creative insights. It will be empowering you, instead of restricting you. It will be a tool that will let you explore your ideas more freely and creatively than it was possible before due to your limitations as a human. That is also why it is so important to get the basic foundations of such an ITP system right, as the limitations of the ITP system will become your limitations.