3 ms·

I am not a professional mathematician but I worked with proof assistants semi-professionally. The problem is that proof assistants doesn't cover everything that

I am not a professional mathematician but I worked with proof assistants semi-professionally. The problem is that proof assistants doesn't cover everything that is required by mathematicians, proofs are often verbose, and unreadable. There's some attempts to alleviate these problems, which are named Homotopy Type Theory, and they are quite successful.

hackermailman 9y ago
Anybody interested, this 2016 paper is a general survey of the current proof logic refinement implementations out there, and the problems and limitations they have which they are currently trying to solve with dependent types/Computational Higher Type Theory http://www.redprl.org/pdfs/afpr.pdf http://www.redprl.org/pdfs/afpr.pdf