17 ms·
Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
- qntmfred 5y agoA quick intro from quanta magazine to Kevin Buzzard's work on computer-assisted proof systems https://www.youtube.com/watch?v=HL7DEkXV_60&t=295s https://www.youtube.com/watch?v=HL7DEkXV_60&t=295s
- lvh 5y agoI recommend the following post, by the author of the proof, for deeper context. Especially near the end, they talk about some of the things they're trying to accomplish with it in plain(ish) English. https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/ https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e...
- deadbeef57 5y agoSee also [1] for a follow-up blogpost that is less technical. [1]: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...
- ajarmst 5y agoThe article is interesting, but that lede is incoherent. Many mathematicians accept computer proofs the way chess grand masters accept computer players. Computer “assistants” that generate proofs that humans cannot follow or understand will always be controversial, and the proofs they generate, even though accepted as valid, will always be decorated with an asterisk.
- 363849473754 5y agoThis is a proof assistant, not an automated theorem prover. The user has to supply* the mathematics and the proof checker formally verifies whether or not the steps are correct. It doesn’t have any creativity (that’s up to the mathematician). *I should have clarified there is some proof generation, see the comment below by opnitro, but I meant the meat and potatoes of novel non-trivial proofs currently has to be supplied by the user.
- ajarmst 5y agoThanks for the clarification.
- opnitro 5y agoThat's not quite true. Many of these proof assistants support some level of automation and proof search. I haven't used Lean specifically, but it's quite common in Coq for projects to write proof search techniques specific to the problem domain and utilize them in their proofs.
- chriswarbo 5y agoTrue, and Isabelle can call out to automated provers (a mechanism called "sledgehammer"!)
- LudwigNagasena 5y agoI don’t understand the chess analogy. How is it in any way similar?
- kevinbuzzard 5y agoLean and the other theorem provers turn mathematical proofs into levels of a computer puzzle game, much like a chess puzzle.
- 6gvONxR4sf7o 5y agoIf not an asterisk, they’ll just have less impact. A proof generates a fact. The best facts and proofs are useful in that they help other things. You work becomes useful for my work, which may become useful for others.
- jacoblambda 5y agoIt's still just as useful. The fact that's proven is what helps other proofs. A computer assisted proof is just as correct or helpful, it just may be more complicated of a proof initially. Given time said proof can be simplified but having the proof in the first place allows you to move away from assumptions into proofs or alternatively even open new doors that weren't known to exist. Keep in mind that these computer aided proofs are equivalent to pen and paper proofs but because you can rely on software to guarantee you haven't made any mistakes, you can make more complex proofs that still work. It's the same as with programming. You can write overly complex and opaque proofs in the same way you can write bad, slow, or hard to read code. It still "works" but it's not ideal and is often a first revision in a series of steps towards the clean, fast, and easy to read final products.
- 6gvONxR4sf7o 5y agoThe best proofs are good explanations as well as just being correct. If you don’t understand the theorem and the proof as well, you’re less likely to use it.
- kevinbuzzard 5y agoPresumably the asterix denotes "actually true"? ;-)
- deleted 5y ago[deleted]
- fjfaase 5y agoFor more details about the actual proof, see: 'Blueprint for the Liquid Tensor Experiment' https://leanprover-community.github.io/liquid/index.html https://leanprover-community.github.io/liquid/index.html
- xvilka 5y agoInteresting choice of the proof assistant though - some specific parts of the Lean's core are not completely decidable, moreover the upcoming Lean 4 version is incompatible with many libraries and proofs written for Lean 3. See also the discussion[1] if the Coq is suitable for number theory as quotients are ubiquitous here. [1] https://github.com/coq/coq/issues/10871 https://github.com/coq/coq/issues/10871
- ulber 5y agoI wasn't aware of Lean not being sound and a quick search didn't come up with anything related to that. Could you link a source?
- martincmartin 5y agoSee other comment. It's sound but not decidable.
- kevinbuzzard 5y agoBasically it turned out that theoretical undecidability did not matter in practice, because Scholze mathematics relies so little on definitional equality. We prove theorems with `simp` not `refl`. Pierre-Marie Pédrot is quoted above as saying that various design decisions are "breaking everything around", but we don't care that our `refl` is slightly broken because it is regarded as quite a low-level tool for the tasks (eg proving theorems of Clausen and Scholze) that we are actually interested in, and I believe our interests contrast quite a lot with the things that Pédrot is interested in.
- kmill 5y agoAnd in "Lean style", refl proofs are a bit distasteful from a software engineering point of view because they pierce through the API of a mathematical object. (In the language of OOP, it can break encapsulation.) It tends to be a good idea to give some definition, then prove a bunch of lemmas that characterize the object, and finally forget the definition.
- Barrin92 5y agoThe abiltiy to automate proofs creates some interesting questions about the nature of mathematics. The article remined me of Erdos saying that you "don't need to believe in God, but you do need to believe in the book", 'the book' here being an imagined collection of mathematical proofs that are so simple, clear and beautiful that they immedieately stand out to any mathematician. I don't mind proof assistants as a way to gain new insights into mathematics, but I worry that maths is drifting into a direction where it turns more into hermeneutics than actual mathematics. The automation of proofs isn't the only thing, I also was very scpetical about the whole process of Shinichi Mochizuki's proof of the abc conjecture.
- deadbeef57 5y agoAs explained in another comment, there is only very mild proof automation going on in this Lean project. Every non-trivial idea has to be supplied to the computer by a human being. The whole circus around Mochizuki's proof of the abc conjecture was dealt with quite well by the social structure of the mathematical community. Many people looked at the proof. Many people got stuck. Several experts got stuck at exactly the same point. And Mochizuki refuses to acknowledge that there is a problem at that point of his "proof". But a consensus was reached in the mathematical community (maybe minus RIMS).
- kungito 5y agoWhat's the name of this point? It's really hard to find any progress on this topic regarding Mochizuki other than some popular articles without any content.
- deadbeef57 5y agoSee https://www.math.columbia.edu/~woit/wordpress/?p=10560 https://www.math.columbia.edu/~woit/wordpress/?p=10560, which links to a technical write-up by Scholze and Stix about what they think is the issue with Mochizuki's proof. Woit's blogpost also gives a bit more links, including a response by Mochizuki.
- gigatexal 5y agoFor anyone frustrated that the article doesn’t say what specific part of math has the most to gain it’s here: “ The crucial point of condensed mathematics, according to Scholze and Clausen, is to redefine the concept of topology, one of the cornerstones of modern maths. A lot of the objects that mathematicians study have a topology — a type of structure that determines which of the object’s parts are close together and which aren’t. Topology provides a notion of shape, but one that is more malleable than those of familiar, school-level geometry: in topology, any transformation that does not tear an object apart is admissible. For example, any triangle is topologically equivalent to any other triangle — or even to a circle — but not to a straight line. Topology plays a crucial part not only in geometry, but also in functional analysis, the study of functions. Functions typically ‘live’ in spaces with an infinite number of dimensions (such as wavefunctions, which are foundational to quantum mechanics). It is also important for number systems called p-adic numbers, which have an exotic, ‘fractal’ topology.”
- dr_kiszonka 5y agoI know nothing about topology. If you have time, could you please explain this sentence? "For example, any triangle is topologically equivalent to any other triangle — or even to a circle — but not to a straight line." Is it because triangles and circles are "2D" and lines aren't?
- yongjik 5y agoCrudely speaking, topologists consider spaces as if they're made of rubber - a mathematically perfect rubber that can be made infinitely thin or stretch to infinity. So, a circle can be made with an infinitely thin circular rubber ring, and you just pinch three points and stretch, and you get your triangle, in any shape. But you can't get a straight line - to do that you need scissors to cut one point of a circle (to be precise, remove a single point) - and then you can stretch the remainder to infinity and now you have your line.
- 77pt77 5y agoNo. Both are 1-d (lines). It's because triangles are loops (closed) and straight lines aren't.
- sabujp 5y ago"Proof assistants can’t read a maths textbook, they need continuous input from humans, and they can’t decide whether a mathematical statement is interesting or profound — only whether it is correct, Buzzard says. Still, computers might soon be able to point out consequences of the known facts that mathematicians had failed to notice, he adds." we're closer to this than people realize
- GPerson 5y agoWhy do you say this?
- kevinbuzzard 5y agoI'm not quite sure what you're asking about. I'm saying that we can't yet take the Wiles and Taylor-Wiles proof of Fermat's Last Theorem, feed it into a machine, and get a Lean proof of Fermat's Last Theorem.
- wolverine876 5y agoI think the GP might have been responding to the GGP, not to your statement in the article.
- GPerson 5y agoHi Kevin, Yes, I was responding to the person who said “we're closer to this than people realize” hoping to learn what they had in mind.
- throwaway81523 5y agoI remember asking Bob Solovay whether he thought Wiles' proof of FLT was within reach of formalization and he said something like: it is probably 20 years away. It may have been 20 years since I asked him that, and seeing this recent work with Lean makes me think FLT might also be doable, which would make Solovay's guess just about spot on.
- kevinbuzzard 5y ago
- SneakyTornado29 5y agoLast time someone talked about automating proofs, a whole new field was invented (computer science)
- denial 5y agoDoes anyone know how condensed mathematics would fit into the modern theory of PDEs (which is heavily based on functional analysis)? Perhaps it's a relic of the sort of math Scholze works on, but it looks far too abstract to provide an impetus for people in those fields to embrace it. Topology, on the other hand, is relatively easy to define and work with (though there are some quirks with dual spaces of continuous linear functionals I've seen aesthetic objections to). Or does it "contain" topology in some sense, allowing people to continue working with notions of convergence obtained from norms?
- deadbeef57 5y agoI think that right now it is not clear why condensed/liquid mathematics would be useful for PDEs. On the other hand, your question > Or does it "contain" topology in some sense, allowing people to continue working with notions of convergence obtained from norms? has a positive answer. You can, if you want, swap out topological spaces, and use condensed sets instead, and just continue with life as usual. At the same time, all of this is in fast paced development, so hopefully we will see some killer apps in the near future. But I expect them more in the direction of Hodge theory and complex analytic geometry.
- wolverine876 5y agoThanks for sharing your expertise. Would you be open to sharing your background? Obviously it's not required, but it would help contextualize what you're saying for the interested non-mathematician; otherwise we're kinda stuck with 'some guy on the Internet said ...' syndrome. :)
- deadbeef57 5y agoSure, I just created an account a couple of days ago, and my favourite username was already taken :oops: I'm Johan Commelin, https://math.commelin.net/ https://math.commelin.net/
- wolverine876 5y ago
- est 5y agois there a simpler version of LEAN suitable for high school student level math? Sympy?
- deadbeef57 5y agoYou might enjoy http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game... It's a game implemented in lean, where you work your way through the basic facts about natural numbers.
- Tainnor 5y agosympy is not a proof assistant, but a symbolic computer algebra system
- Tainnor 5y agoThis is going to be an exciting area. I spent some time previously playing with Coq. It's very powerful, but even proving the simplest undergraduate maths statements (say, about group theory) can prove very challenging. I believe that part of this is that Coq uses different mathematical foundations than traditional mathematics, which mostly uses set theory (ZFC, although most people don't care about the specifics). So it can be hard or unnatural to express something like "subgroup". I don't know if Lean fares better in that respect. Coq documentation is also IMHO almost impossible to understand unless you're already very deeply knowledgeable about the system. We will probably still need some more iterations, to get more user friendly assistants with better documentation and to get adequate teaching resources etc.
- raphlinus 5y agoLean's foundations are similar to Coq. I think the ergonomics are a bit better. Most activity in proof systems is based in type theory these days, but set theoretical systems do exist, of which Metamath is the most mature. That said, Metamath is seriously lacking in automation, so there is an element of tedium involved. That's not because of any fundamental limitations, but I think mostly because people working in the space are more motivated to do things aligned with programming language theory. There was also a talk by John Harrison a few years ago proposing a fusion of HOL and set theory, but I'm not sure there's been much motion since then. I believe a fully featured proof assistant based in set theory would be a great contribution. [1]: http://aitp-conference.org/2018/slides/JH.pdf http://aitp-conference.org/2018/slides/JH.pdf
- robinzfc 5y agoIt depends on what you mean by "fully featured" but Isabelle supports ZF logic [1] and also you can do ZFC in Isabelle/HOL [2]. And, of course there is Mizar [3]. [1] https://isabelle.in.tum.de/dist/library/ZF/ZF/index.html https://isabelle.in.tum.de/dist/library/ZF/ZF/index.html [2] https://www.isa-afp.org/entries/ZFC_in_HOL.html https://www.isa-afp.org/entries/ZFC_in_HOL.html [3] http://mizar.org/ http://mizar.org/
- Ericson2314 5y ago
- mjreacher 5y agoIs there any opportunity for interested undergrads to learn about this more (since I doubt we could contribute)?
- foooobar 5y agoIf you're interested in interactive theorem proving with Lean (and not condensed mathematics), the Lean community landing page is a good place to start. https://leanprover-community.github.io/ https://leanprover-community.github.io/ Especially the "Natural Number Game" under "Learning resources" has been successful in teaching folks the very basics for writing proofs. Once finished, a textbook like "Theorem Proving in Lean" can teach the full basics. Feel free to join the Lean Zulip at any point and ask questions at https://leanprover.zulipchat.com/ https://leanprover.zulipchat.com/ in the #new members stream. Mathlib has plenty of contributions from interested undergrads :)
- FabHK 5y agoTIL: Fields medallists ask questions on MathOverflow... [1] This has me in awe about the depth of mathematics, the pace of progress, the miracle of specialisation. I have a degree in an applied-math-y adjacent field, and understand nothing. (And, btw, I was astonished how knowledgable some commenters right here were, and then realised that we have the (co-)authors of the results themselves here! gotta love HN.) With that said, here some (non-mathematical) snippets I found interesting (apart from the great word "sheafification"): > Why do I want a formalization? > — I spent much of 2019 obsessed with the proof of this theorem, almost getting crazy over it. In the end, we were able to get an argument pinned down on paper, but I think nobody else has dared to look at the details of this, and so I still have some small lingering doubts. > — while I was very happy to see many study groups on condensed mathematics throughout the world, to my knowledge all of them have stopped short of this proof. (Yes, this proof is not much fun…) > — I have occasionally been able to be very persuasive even with wrong arguments. (Fun fact: In the selection exams for the international math olympiad, twice I got full points for a wrong solution. Later, I once had a full proof of the weight-monodromy conjecture that passed the judgment of some top mathematicians, but then it turned out to contain a fatal mistake.) > — I think this may be my most important theorem to date. (It does not really have any applications so far, but I’m sure this will change.) Better be sure it’s correct… > In the end, one formulates Theorem 9.5 which can be proved by induction; it is a statement of the form ∀∃∀∃∀∃ (\forall \exists \forall \exists \forall \exists), and there’s no messing around with the order of the quantifiers. It may well be the most logically involved statement I have ever proved. > Peter Scholze, 5th December 2020 [2] Question: What did you learn about the process of formalization? Answer: I learnt that it can now be possible to take a research paper and just start to explain lemma after lemma to a proof assistant, until you’ve formalized it all! I think this is a landmark achievement. Question: And about the details of it? Answer: You know this old joke where a professor gets asked whether some step really is obvious, and then he sits down for half an hour, after which he says “Yes, it is obvious”. It turns out that computers can be like that, too! Sometimes the computer asks you to prove that A=B, and the argument is “That’s obvious — it’s true by definition of A and B.” And then the computer works for quite some time until it confirms. I found that really surprising. Question: Was the proof in [Analytic][4] found to be correct? Answer: Yes, up to some usual slight imprecisions. Question: Were any of these imprecisions severe enough to get you worried about the veracity of the argument? Answer: One day I was sweating a little bit. Basically, the proof uses a variant of “exactness of complexes” that is on the one hand more precise as it involves a quantitative control of norms of elements, and on the other hand weaker as it is only some kind of pro-exactness of a pro-complex. It was implicitly used that this variant notion behaves sufficiently well, and in particular that many well-known results about exact complexes adapt to this context. There was one subtlety related to quotient norms — that the infimum need not be a minimum (this would likely have been overlooked in an informal verification) — that was causing some unexpected headaches. But the issues were quickly resolved, and required only very minor changes to the argument. Still, this was precisely the kind of oversight I was worried about when I asked for the formal verification. Question: Were there any other issues? Answer: There was another issue with the third hypothesis in Lemma 9.6 (and some imprecision around Proposition 8.17); it could quickly be corrected, but again was the kind of thing I was worried about. The proof walks a fine line, so if some argument needs constants that are quite a bit different from what I claimed, it might have collapsed. Question: Interesting! What else did you learn? Answer: What actually makes the proof work! When I wrote the blog post half a year ago, I did not understand why the argument worked, and why we had to move from the reals to a certain ring of arithmetic Laurent series. [...] Question: So, besides the authors of course, who understands the proof now? Answer: I guess the computer does, as does Johan Commelin. [Note: = deadbeef57 here on HN][3] [1] https://mathoverflow.net/questions/386796/nonconvexity-and-discretization https://mathoverflow.net/questions/386796/nonconvexity-and-d... [2] https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/ https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e... [3] https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-... [4] http://www.math.uni-bonn.de/people/scholze/Analytic.pdf http://www.math.uni-bonn.de/people/scholze/Analytic.pdf
- hansor 5y agoThey did the same with Prolog in 70" and... failed. Nothing new.
- contrarian_5 5y agoi love the time that we live in. people talk about there being a glut of podcasts, but i can type "Peter Scholze" into youtube and there is a full hour-long interview with him hosted by another mathematician. you can see her channel is very new and almost certainly a part of this latest wave of pandemic podcasters. its so great to take an interest in a random person from a nature article and be able to immediately get a visceral idea of who he is and what hes about. https://www.youtube.com/watch?v=HYZ3reRcVi8 https://www.youtube.com/watch?v=HYZ3reRcVi8
- bpcpdx 5y agoThis kinda gives me chills because I can't help but think of Warhammer 40k. Essentially our civilization progressed to the point where computers started to take more of a role in new discoveries much like in the real world. As computers got more powerfull and AI developed naturally scientific advancement sped up. But there came a point when the science and math became too advanced for humans to even comprehend, so computers did it. Then there came a point when things were so advanced that even scientists couldn't even ask the right questions so an AI intermediate would have to be used. Then things get weird and you have the 40k universe. Anyways I know I probably butchered it a little but that's the gist of it and I can totally see things progressing in the real world up to the point where things get weird in 40k.
- runeks 5y ago> But systems known as proof assistants go deeper. The user enters statements into the system to teach it the definition of a mathematical concept — an object — based on simpler objects that the machine already knows about. A statement can also just refer to known objects, and the proof assistant will answer whether the fact is ‘obviously’ true or false based on its current knowledge. As far as I can see this is just programming. How is this different from writing in Java int i = “hello” and seeing that the Java compiler rejects this “thesis”? Of course, we need more complex types than “int” and “String”, but in principle it’s the same.
- fspeech 5y agoYes and the isomorphism is known as Curry-Howard Correspondence https://en.wikipedia.org/wiki/Curry-Howard_correspondence https://en.wikipedia.org/wiki/Curry-Howard_correspondence
- zant 5y agoYeah you can say that. You can also say that Machine Learning is just programming. Or in a similar way you can also say that First Order Logic is just programming. However, the cool thing about programming is that it lets us represent a lot of different things. In this case you're representing the construction and interaction of mathematical objects, with a language that targets a specific proof management system to verify this constructions. But yes, it is "just programming", and some functional languages even support proofs to some extent like Scala or Agda.
- AtlasBarfed 5y agoThe Lean version of the theorem was 10,000s lines of code... With verifiers like this as a useful tool, I'm guessing in the coming years this LoC will be dwarfed. I'm a bit surprised a theorem of major complexity reduced to that small a LoC count.