Tag Archives: proofs

Proof assistants and the future of math

Are proof assistants the next breakthrough in mathematics? This is a question I have been thinking about since I tried the Lean proof assistant. I have tried proof assistants before, but Lean feels like it’s on another level. For one, I actually wrote a natural deduction proof in it. I can easily imagine it being […]

Some thoughts on proof assistants

A proof assistant is a computer program that takes as input a proof in a formal language and outputs true if and only if the proof is a valid proof in a formal system. An example would be first-order logic with its inference rules. Proof assistants are supposed to tell you whether your proof is […]