News for hackers. Stuff that matters.

A comment on Why is writing mathematical proofs more fault-proof than writing code? (2011). Parent comment

Re:Why is writing mathematical proofs more fault-proof than ... by solomatov on Monday January 01, 2018 @11:02AM (#16046525)
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.

[ Parent | on HN ]
Re:Why is writing mathematical proofs more fault-proof than ... by hackermailman on Monday January 01, 2018 @04:16PM (#16048098)
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
[ Parent | on HN ]