4 ms·
Once upon a time, the professor of a class on logic I was taking pointed out that, if you proved some famous open conjecture (I think Fermat's was the example)
by mcguire 3y ago
Once upon a time, the professor of a class on logic I was taking pointed out that, if you proved some famous open conjecture (I think Fermat's was the example) using some simple proof that everyone had just missed so far, mathematicians would pat you on the head, maybe give you an award or something, and you (and the conjecture) would become another forgotten footnote.
Major mathematical advances come from difficult problems when a new branch of mathematics is invented to solve them. Think of calculus, non-Euclidean geometry, and Turing machines (and their equivalents).
The problem I see with Coq, the proof checker I've worked with the most, and the others I've seen is that the proofs they result in are neither good, understandable programs nor good, understandable proofs. They are as complicated as complex programs, but written in something that isn't a half-way clean programming language, but they're also not written as a traditional proof. That goes back up to the article's point that the purpose of a proof is to convince and enlighten others.
Sure, I'd have to say a proposition proven in Coq is true, but how do you get from that to the ideas in the proof letting you go on to other problems?
- madsbuch 3y agoI don't think the point is to either have good math or good code. When you develop software in Coq and the likes, it is library code. It is high impact code that is guaranteed to be correct. It is written once and not maintained – You would never build the new Twitter in Coq. When you develop math on Coq, you build abstractions. You just need to know that theorems that you are working on. Then you pull in all the lemmas in coq to help you solve that theorem. You do not need to understand the lammas coq uses to help you prove your theorem – coq does that for you. So your math is extremely concise. This is in opposition to normal math, where you need to be able to explain the hierarchy your theorem works on top of.
- hgsgm 3y agoNormal math also concisely cites pre-existing theorems
- infogulch 3y agoAh but normal math is a social compact in a way that computer-aided proofs are not. Very few handwritten proofs are actually written down in detail, and there are various cases where attempting to do so actually failed or required new work to actually close the gap.
- trenchgun 3y agoProof assistants assist with normal math. They just make the normal formal and realiable.
- mcguire 3y ago"It is written once and not maintained..." Be careful, this is how you get the Ariane V first flight. "You do not need to understand the lammas coq uses to help you prove your theorem..." If I wanted to generalize your theorem or move it to some other base abstraction, the first thing I need to do is to read and understand your proof. If that proof is made up of Coq tactics chosen based on "whatever works", I'm going to have a bad day. Now, many results especially in CS are made by reducing a new problem to an existing theorem, but I don't know how well that works as a general case.
- sebzim4500 3y agoI guess the hope is that eventually there will be a language which is roughly as easy to read/write as normal proofs in English but can be machine checked. Lean comes closer than Coq, but is still far from this ideal. It may be that AI will need to be involved (as in, there could be a tactic that generates proof terms using an transformer or something).
- hgsgm 3y agoLike Cobol? Coqobol?
- zozbot234 3y ago> I guess the hope is that eventually there will be a language which is roughly as easy to read/write as normal proofs in English but can be machine checked. That's what "declarative proofs" are for (as seen in Mizar, Isar, and formerly in the Coq plugin C-zar). Most proofs in interactive proof assistants are written as "proof scripts", which cannot be understood without playing them back in the proof assistant (in fact, specifically the version of the proof assistant that the "script" was originally written for) and checking how each step in the "script" relates to the current proof state. Declarative proofs are more self-contained, in that the assumptions and conclusions involved in each proof step can be ascertained by just reading them in the code. They can also be naturally simplified into structural "proof sketches", where missing steps in the proof could potentially be filled by a proof-searching "AI".
- creata 3y ago> in fact, specifically the version of the proof assistant that the "script" was originally written for Are Isar updates guaranteed not to break proofs?
- edflsafoiewq 3y agoI think you'll get machines that can check human proofs first.
- sebzim4500 3y ago
- passion__desire 3y agoThere is something similar Nima Arkani-Hamed talks about Feynman equations during his amplituhedron lecture, pages and pages of equations being reduced to simple representation. @56:26 in https://youtu.be/sv7Tvpbx3lc https://youtu.be/sv7Tvpbx3lc
- jiggawatts 3y agoIronically, I consider the amplituhedron to be very unclear. Every presentation by its author goes: "here's a triangle, here's a simplex, and now... ta-da... the amplituhedron is the same!" He skips 15 steps every time. It's literally the "here's a circle, then another circle, and now just draw the rest of the owl", but in terms of theoretical physics.
- passion__desire 3y agoHe says in the lecture that physicists arrived at the simple representation by studying Feynman diagrams and looking at how terms cancel each other. And amplituhedron also gives rise to those same representation. This is the reason why he considers amplituhedron to be a good research path. He cites similar interpretation change that happened before in physics[0] [0] : https://youtu.be/sv7Tvpbx3lc?t=2664 https://youtu.be/sv7Tvpbx3lc?t=2664