3 ms·
If only we had automated proof assistants that could check the proof quickly. Oh wait.
by adamnemecek 9y ago
If only we had automated proof assistants that could check the proof quickly. Oh wait.
- monochromatic 9y agoUnfortunately, coq can’t parse just anything.
- dogecoinbase 9y agoThis comment does nothing other than demonstrate your own ignorance of research mathematics.
- adamnemecek 9y agoPlease keep going.
- deleted 9y ago[deleted]
- reallydude 9y agoWhy bother?
- qmalzp 9y agoI have never seen a theorem prover applied to even basic 100-year-old results in Algebraic Number Theory. I think you underestimate the difficulty in translating a mathematical idea into a format a computer program can understand.
- dang 9y agoPlease don't post snarky dismissals to Hacker News. I'm dismayed to see this from you here.
- bo1024 9y agoUnfortunately at this juncture, it's extremely difficult and time-consuming to place an arbitrary proof in the language of proof assistants. It's a very noble goal and much respect to those who do it, but even fully formalizing something like the four-color theorem is a major accomplishment.