News for hackers. Stuff that matters.

A comment on Formalising a new proof that the square root of two is irrational.

Re:Formalising a new proof that the square root of two is ir... by bdrum on Thursday January 19, 2023 @03:14AM (#34437917)
Looks very cool, but what I've wondered - there is any other tool like Isabelle? upd. https://en.wikipedia.org/wiki/Proof_assistant
[ Parent | on HN ]
Re:Formalising a new proof that the square root of two is ir... by ykonstant on Thursday January 19, 2023 @06:18AM (#34439114)
In the mathematical community, the best known proof assistants are Coq, Lean and Isabelle.
[ Parent | on HN ]