Re:Formalising Mathematics: An Introduction
by _ouml_ on Monday February 22, 2021 @12:24AM
(#26221175)
Yes, these systems are being used to formally verify implementations of cryptographic protocols, or implementations of numerical algorithms, for example.
Note that there are two distinct components that interact: (i) verification of proofs and (ii) automation of finding the proofs. The latter is very much an active field of research, but so far isn't of the level that it will prove most of your theorems for you.
Re:Formalising Mathematics: An Introduction
by yoneda on Sunday February 21, 2021 @08:54PM
(#26219799)
> but can't typically "find their own way" to the proof of a theorem
That's not what proof assistants like Lean and Coq are about. Sure, they can automate some trivial things, but generally their main utility is that they check your reasoning, not come up with it for you.
As an economist, I sometimes want to prove things that a real mathematician could do in their sleep. There's Mathematica and friends, but they have their limitations, i.e. they can do what you tell them but can't typically "find their own way" to the proof of a theorem. Might these systems ever come down to my level?