3 ms·
And additionally it takes a lot of effort to formalise a proof. (I say this as someone who has spent nearly two years formalising basic maths in Agda.) It's tru
by Smaug123 7y ago
And additionally it takes a lot of effort to formalise a proof. (I say this as someone who has spent nearly two years formalising basic maths in Agda.) It's true in maths as in programming: 90% of the work is in the last 10%, and if you don't get the last 10%, you haven't got a proof.
- zozbot234 7y agoThe usual rule of thumb is that 1 page of paper proof leads to 4 pages of "proper" formal proof. Though this may vary depending on how capable the proof assistant is - AIUI, Agda requires you to write out complete proof terms, whereas other systems may be more capable. Sometimes you can use a kind of "reflection" that makes many proofs trivial, simply by defining a decision procedure that's proven to be correct in the general case, and having the system perform the appropriate computations. This is how you would deal, e.g. with trivial simplifications in elementary algebra (that can usually be proven to be valid in any ring, field etc.)
- Smaug123 7y agoCorrect, Agda has this notion of reflection. The way to do "tactics" in Agda is simply to manipulate expressions, and there's no meta-language in which to do this: it's just Agda all the way down. It's neat, but not easy.