3 ms·
Outsider's question: is it likely that projects like Lean and Coq will ever feed into stuff that applied researchers find useful? By applied researchers I don't
by dash2 6y ago
Outsider's question: is it likely that projects like Lean and Coq will ever feed into stuff that applied researchers find useful? By applied researchers I don't mean "applied mathematicians" but scientists who use maths in their field.
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?
- deleted 6y ago[deleted]
- yoneda 6y ago> 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.
- _ouml_ 6y agoYes, 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.