14 ms·

Formalising Mathematics: An Introduction

205 points by panic 6y ago

fjfaase 6y ago
I think that something like http://us.metamath.org/index.html http://us.metamath.org/index.html has already gone a long way in formalizing math. And this is not the only attempt to formalize math, but it is unique that it uses a very limited amount of syntax and rules, and makes use of a simple (small) proof engine, which makes verifying that the proof engine is correct possible.
- JadeNB 6y ago
  A small proof engine, and maybe a limited amount of rules (depending on the exact technical meaning of 'rules') is a good thing, but I'd say a limited amount of syntax is a bad thing. Mathematicians as a community tend to be happy with—I might even say to prefer—lots of syntax, and, if you want to get a formalisation process really going, layering it with enough syntactic sugar to bring in mathematicians who aren't usually 'formalisers' is going to be essential. It's also true that there are lots of attempts at formalisation out there; I happen to know about vdash.org , for example, but there are certainly others. I think it's good to have an abundance of formalisations, since no one formalisation style is going to appeal to everyone (for example, as already discussed above, probably the more formalisation-minded mathematicians will have a higher tolerance for minimalism).
- Gehinnn 6y ago
  Lean allows for third party type checkers. There are relatively small alternative type checkers for Lean (e.g. a scala implementation [1]). Lean's power lies in its elaborator that breaks down complex tactic-based proofs to a core proof language. This elaboration process can be extended with custom tactics and custom syntax, making it way more powerful than metamath. [1] https://github.com/gebner/trepplein/tree/master/src/main/scala/trepplein https://github.com/gebner/trepplein/tree/master/src/main/sca...
- kevinbuzzard 6y ago
  The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving that from the axioms of a ring directly in metamath, I challenge you to do it in fewer than 30 moves. I should also say that whilst Metamath has certainly formalised a whole bunch of mathematics, it has not remotely gone "a long way" by any reasonable measure which a mathematician would use. For example, how much of an undergraduate mathematics curriculum does it have? How much representation theory? None. How much differential geometry? None. How much commutative algebra? Epsilon. These are the measures which mathematicians use, not lines of code. It is time that formalisation started to appeal to mathematicians, and for this to happen it is essential that it starts to demonstrate that it can actually do a lot of the kind of mathematics which is recognised as "completely standard undergraduate material and hence trivial" by mathematicians. It is still the case that these systems cannot do certain things which were known to Gauss or Euler (for example it was only this year that Lean learnt the proof that the class group of an imaginary quadratic field was finite, and as far as I know no other system at all has class groups -- but we teach this to the undergraduates!). Just saying "large code base therefore we've gone a long way" is not the correct logic. The question is how much of it is recognisable as worth teaching to undergraduates in 2021, and conversely how much stuff worth teaching to undergraduates in 2021 is _not_ in any of these systems. That's where the problems begin to show up. In Lean we are well into a project of formalising an entire undergraduate curriculum and within about two years we will have finished.
  - dwheeler 6y ago
    > The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving that from the axioms of a ring directly in metamath, I challenge you to do it in fewer than 30 moves. While it's allowed, generally Metamath users do not prove constructs directly from axioms, for exactly the same reason as you don't do it in Lean or traditional informal mathematics. You're right that most Metamath tools have fewer automated tactics, but there are tools with some automation, and people are working to improve that.
adamnemecek 6y ago
I wish these attempts were using constructive mathematics but I understand that that would turn away a lot of mathematicians.
- JadeNB 6y ago
  Just pick a different one! There are definitely formalisation efforts out there that use constructive mathematics; for example Coq is so called after the logic, the calculus of constructions, that it uses (https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions).
  - kevinbuzzard 6y ago
    Hi! Yes! Just pick a different one! The problem is that constructivists have been formalising mathematics for decades and have not really managed to break through into the mainstream mathematical community with their efforts. The difference with Lean's maths library is that we absolutely reject constructivism, which makes Lean far less suitable for certain kinds of computations but conversely far far better equipped for proving all the theorems in an undergraduate mathematics curriculum and then going on to tackle research level mathematical questions of the kind which most mathematicians recognise as "normal mathematics". My argument (I should say that I am the author of the blog post) is that this resolutely non-classical approach is far more likely to arouse the interest of mainstream mathematicians, who rejected constructivism 100 years ago and have never looked back. I can certainly see a role for constructive mathematics, however I know from experience that most working mathematicians reject it and hence the pragmatic approach is to reject it when formalising if we are to start appealing to the mathematical masses.
    - guerrilla 6y ago
      The Four Colour Theorem in Coq seems pretty mainstream I'd say... Also I guess you know that you don't personally have to reject LEM to use Agda or whatever, you just can't do everything in it or at least everything the classical way.
RedouaneBrahimi 6y ago
Novak Djokovic Wins Third Straight Australian Open Title https://snip.ly/8mepd7#https://www.nytimes.com/2021/02/21/sports/tennis/novak-djokovic-wins-australian-open.html https://snip.ly/8mepd7#https://www.nytimes.com/2021/02/21/sp...
- JadeNB 6y ago
  Wrong thread?
  - mckirk 6y ago
    No, it's probably just a good idea to remind people of this feat, similarly to the legendary wrestling match in nineteen ninety-eight when The Undertaker threw Mankind off Hell In A Cell and plummeted 16 ft through an announcer's table.
schoen 6y ago
A game to try this out (by Kevin Buzzard, who is participating in this thread and is also the author of this blog post). https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam... I loved it and have been trying to make some subsequent levels about divisibility.
- uyt 6y ago
  I played it recently. I spent almost a full day to finish all the worlds and then lost interest afterwards. I think I had expectations that it would be a lot less ... tedious? Like I was hoping it would be mostly automated except needing hints whenever it got stuck. Much like how the flavor text would hint to you (the human) that you needed to use certain theorems for certain levels. Instead, it was so low level that you had to do every step of algebra manually with a line of code each. (and to be fair, in the beginning it was necessary because you're developing the usual rules of algebra as you go, but even in the later levels after they tell you about the ring tactic there's still a lot of manual algebra you need to do) The search space seems small enough that even I was just mindlessly spamming rewrite/intro/apply/induction. Why can't a computer automate this completely. And going in the other direction, I was hoping this would be a good tool to aid in proofwriting. But most of the "proof" I wrote was complete gibberish not meant for human consumption. I think the problem is because the code relies heavily on mutating a context that you can't see without using the lean UI. Anyway, maybe the number game is just not a good intro to the full capabilities of lean and I am missing the point.
  - ahelwer 6y ago
    No, I think you have a pretty good grasp of things. In the real world people do use more powerful tactics like ring to skip all the low-level algebraic manipulation (which I personally really enjoyed but can see others finding tedious). Your point about proof readability applies to interactive theorem provers generally. You can see a tradeoff here between Lean/Coq and more "literate" formal proof languages like TLA+, which has a prover called TLAPS (TLA+ Proof System). TLA+ proofs are written in a hierarchical style Lamport proposed in his paper How to Write a 21st Century Proof[0], and are readable by themselves. The BIG BIG tradeoff here is that when you're writing the proof in TLA+, it's very difficult to know what the prover is "thinking" and why it is stuck. Whereas with interactive provers you know exactly what the prover is "thinking" - the proof consists solely of instructions to manipulate those thoughts which you see on screen at all times! So at this time it seems there's a tradeoff between ease of writing a formal proof and ease of reading a formal proof. [0] https://www.microsoft.com/en-us/research/publication/write-21st-century-proof/ https://www.microsoft.com/en-us/research/publication/write-2...
zant 6y ago
I absolutely love everything about this. Specially how it can provide access to knowledge to people all around the world. I'm currently thinking about getting a degree in Maths, and I find extremely appealing the notion of having a repo of knowledge from where to gather theorems, specially useful for newer developed areas.
breck 6y ago
I will pay $3.14 to the first person that formalizes mathematics using only https://treenotation.org/ https://treenotation.org/.
- drdeca 6y ago
  This appears to just be saying “using python style indentation to represent trees”? I don’t understand the significance. Like, yeah, you can express whatever tree you want that way. Plenty of other ways to represent trees. It’s a nice enough default if you don’t know anything about the sort of thing the tree will contain. But there’s a reason that when writing conditionals, we don’t put each symbol in the expression on their own line. Those also have their own tree structure, they are also part of the AST, but we put many of the nodes on the same line for ease of reading and editing.
  - breck 6y ago
    > But there’s a reason that when writing conditionals, we don’t put one symbol in the expression on their own line I won't disagree with you. However when you zoom out and crunch the numbers, you'll find that although there are infinite expressions to put in conditionals, in practice an absolutely minuscule amount of those patterns are actually used. Context free grammars are not free. Better ways are coming.
carapace 6y ago
The only major problem (IMO) is that Lean and the others (Coq, Hol, Isabelle, Agda, Idris, etc...) are all pretty hard to read. Check out "Automated Propositional Sequent Proofs in Your Browser with Tau Prolog" for a promising approach: https://www.philipzucker.com/javascript-automated-proving/ https://www.philipzucker.com/javascript-automated-proving/ It's rendering LaTeX proof trees.
- nynox 6y ago
  Following this proof tree idea, this recent paper https://arxiv.org/abs/2102.03044 https://arxiv.org/abs/2102.03044 suggests to think of proofs of theorems as large trees, a tiny subset of which needs to be made explicit to convey the confidence the rest could be written out (if ever needed).
  - carapace 6y ago
    Does that presuppose that it's computationally expensive to verify proofs? If so, isn't that kind of unrealistic?
    - nynox 6y ago
      Verifying fully formalized proofs is cheap. What is expensive is to produce such formalized proofs. More precisely, to formalize a proof written in a typical math paper is extremely time-consuming and not so informative (that's why it's almost never done in practice).
      - carapace 6y ago
        Ah, cheers. :) But doesn't that bring us full-circle to Buzzard's point? Isn't that why he's saying, "Hey gang, let's do math with machines." in the first place?
- asdftemp 6y ago
  that is a neat demo with a lot of useful links! In fact, it seems that the Lean developers/community are very interested in new methods of achieving readability, and providing users with tools to build interfaces that scale up to the complexity of real workflows. For example, Lean in vscode supports interactive html "widgets": https://youtu.be/8NUBQEZYuis?t=453 https://youtu.be/8NUBQEZYuis?t=453 (at that timestamp, there's a quick introduction to their typical use at the moment). lean4 is committed to all sorts of extensibility; here's a demonstration of the new macros: https://twitter.com/derKha/status/1354082976456441861 https://twitter.com/derKha/status/1354082976456441861. There have also been several instances of users implementing old lean3 features (for example, the `calc` tactic mode, which has unique syntax for proving (in)equalities) by simply defining new type classes and short macros.
bsdz 6y ago
Last month Kevin Buzzard gave an interesting talk "How do you convince mathematicians a theory prover is worth their time?" about how he became involved with LEAN and some of the proofs he formalised with it: https://youtu.be/8PLrxAfmC_o https://youtu.be/8PLrxAfmC_o
- deleted 6y ago
  [deleted]
- infogulch 6y ago
  During Q&A there was a friendly quarrel about 'mainstream' vs 'constructive' maths. I think there's a funny analogy in here, if you let: mainstream proof : constructive proof :: program code : machine code then Kevin is arguing that the idea of actually compiling his beautiful algorithms into machine code is silly, and that compiling program code in general is rather pointless.
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 ago
  Yes, 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.
317070 6y ago
> However, AI works best with a database — and those databases are not yet there. They do, but I would tell you that if that is your main motivation to create those databases, don't do it. The AI might spend milliseconds on work that takes man-years to compile, but get stuck on absolutely tiny issues of details it can't grok and which you can quickly explain. If AI is the goal, I would propose to discuss with AI-researchers in the area of automated maths about what they can actually use to make progress. There are ways to have the AI learn unsupervised as much as possible, and to have it ask for supervision where needed. In a similar way, it took a while to teach alphaGo to play go, but it only took a couple of extra years to have alphaZero play both go and chess without any database of example games. I fully agree with the rest of the argument and I love the work that is being done to double check mathematics. But as AI researcher, I think this is a poor motivation and would warn against using it, as it might be very disappointing in the long run about how little of it turned out to be useful for AI.
- voxl 6y ago
  If you read the article you can tell that AI is not the goal, it is a byproduct of the goal. The goal is to have confidence in the correctness of mathematical results proved by other experts. Also, there has _already_ been some success on using AI to find proofs in lean.
- _ouml_ 6y ago
  There is a very active community around Lean ranging from mathematicians with no clue about computers to AI researchers trying to improve the automation. These AI researchers have explicitly said that bigger training sets will be very helpful. But like the sibling comment says, AI is not the main point.
btilly 6y ago
If anyone wants of a concrete reason to formalize mathematics, consider this. The classification of finite simple groups is a major result in mathematics that is a foundation for many others. See https://en.wikipedia.org/wiki/Classification_of_finite_simple_groups https://en.wikipedia.org/wiki/Classification_of_finite_simpl... for more. However at the time the proof was finishing, people were leaving the field, and the very people who proved it did not feel that their results were checked. They were not confident of the result. And nobody has been able to review the proof. This began a decades long effort, which is currently incomplete, to produce a second proof that is more understandable. That effort seems to have fizzled out. So one of the most important results in mathematics in the 20th century does not have a proof that anyone can understand or review. And this is true despite a number of very smart people devoting their entire lives to the subject. I maintain that no amount of human verification and re-verification will result in my being as confident of this result as I am about most mathematical results that I know. The only way to actually make this into something we should be confident of is to translate the existing proofs to something computer checkable.
- edanm 6y ago
  > I maintain that no amount of human verification and re-verification will result in my being as confident of this result as I am about most mathematical results that I know. The only way to actually make this into something we should be confident of is to translate the existing proofs to something computer checkable. Or to indeed find that simpler proof, I suppose? (Not disagreeing with anything you're saying, just checking - it's a fascinating story that I didn't know about this topic)
  - schoen 6y ago
    I don't understand this area well at all, but I know the existing classification of finite simple groups is very long and detailed. Wikipedia says > The proof consists of tens of thousands of pages in several hundred journal articles and that the second-generation simplified version might possibly run to only 5,000 pages. 5,000 pages of math is easier to understand and/or believe in than tens of thousands of pages, but it's still a pretty daunting amount even for specialists.

205 points by panic 6y ago

I think that something like http://us.metamath.org/index.html http://us.metamath.org/index.html has already gone a long way in formalizing math. And this is not the only attempt to formalize math, but it is unique that it uses a very limited amount of syntax and rules, and makes use of a simple (small) proof engine, which makes verifying that the proof engine is correct possible.

JadeNB 6y ago
A small proof engine, and maybe a limited amount of rules (depending on the exact technical meaning of 'rules') is a good thing, but I'd say a limited amount of syntax is a bad thing. Mathematicians as a community tend to be happy with—I might even say to prefer—lots of syntax, and, if you want to get a formalisation process really going, layering it with enough syntactic sugar to bring in mathematicians who aren't usually 'formalisers' is going to be essential. It's also true that there are lots of attempts at formalisation out there; I happen to know about vdash.org , for example, but there are certainly others. I think it's good to have an abundance of formalisations, since no one formalisation style is going to appeal to everyone (for example, as already discussed above, probably the more formalisation-minded mathematicians will have a higher tolerance for minimalism).
Gehinnn 6y ago
Lean allows for third party type checkers. There are relatively small alternative type checkers for Lean (e.g. a scala implementation [1]). Lean's power lies in its elaborator that breaks down complex tactic-based proofs to a core proof language. This elaboration process can be extended with custom tactics and custom syntax, making it way more powerful than metamath. [1] https://github.com/gebner/trepplein/tree/master/src/main/scala/trepplein https://github.com/gebner/trepplein/tree/master/src/main/sca...
kevinbuzzard 6y ago
The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving that from the axioms of a ring directly in metamath, I challenge you to do it in fewer than 30 moves. I should also say that whilst Metamath has certainly formalised a whole bunch of mathematics, it has not remotely gone "a long way" by any reasonable measure which a mathematician would use. For example, how much of an undergraduate mathematics curriculum does it have? How much representation theory? None. How much differential geometry? None. How much commutative algebra? Epsilon. These are the measures which mathematicians use, not lines of code. It is time that formalisation started to appeal to mathematicians, and for this to happen it is essential that it starts to demonstrate that it can actually do a lot of the kind of mathematics which is recognised as "completely standard undergraduate material and hence trivial" by mathematicians. It is still the case that these systems cannot do certain things which were known to Gauss or Euler (for example it was only this year that Lean learnt the proof that the class group of an imaginary quadratic field was finite, and as far as I know no other system at all has class groups -- but we teach this to the undergraduates!). Just saying "large code base therefore we've gone a long way" is not the correct logic. The question is how much of it is recognisable as worth teaching to undergraduates in 2021, and conversely how much stuff worth teaching to undergraduates in 2021 is _not_ in any of these systems. That's where the problems begin to show up. In Lean we are well into a project of formalising an entire undergraduate curriculum and within about two years we will have finished.
- dwheeler 6y ago
  > The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving that from the axioms of a ring directly in metamath, I challenge you to do it in fewer than 30 moves. While it's allowed, generally Metamath users do not prove constructs directly from axioms, for exactly the same reason as you don't do it in Lean or traditional informal mathematics. You're right that most Metamath tools have fewer automated tactics, but there are tools with some automation, and people are working to improve that.

adamnemecek 6y ago

I wish these attempts were using constructive mathematics but I understand that that would turn away a lot of mathematicians.

JadeNB 6y ago
Just pick a different one! There are definitely formalisation efforts out there that use constructive mathematics; for example Coq is so called after the logic, the calculus of constructions, that it uses (https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions).
- kevinbuzzard 6y ago
  Hi! Yes! Just pick a different one! The problem is that constructivists have been formalising mathematics for decades and have not really managed to break through into the mainstream mathematical community with their efforts. The difference with Lean's maths library is that we absolutely reject constructivism, which makes Lean far less suitable for certain kinds of computations but conversely far far better equipped for proving all the theorems in an undergraduate mathematics curriculum and then going on to tackle research level mathematical questions of the kind which most mathematicians recognise as "normal mathematics". My argument (I should say that I am the author of the blog post) is that this resolutely non-classical approach is far more likely to arouse the interest of mainstream mathematicians, who rejected constructivism 100 years ago and have never looked back. I can certainly see a role for constructive mathematics, however I know from experience that most working mathematicians reject it and hence the pragmatic approach is to reject it when formalising if we are to start appealing to the mathematical masses.
  - guerrilla 6y ago
    The Four Colour Theorem in Coq seems pretty mainstream I'd say... Also I guess you know that you don't personally have to reject LEM to use Agda or whatever, you just can't do everything in it or at least everything the classical way.

RedouaneBrahimi 6y ago

Novak Djokovic Wins Third Straight Australian Open Title https://snip.ly/8mepd7#https://www.nytimes.com/2021/02/21/sports/tennis/novak-djokovic-wins-australian-open.html https://snip.ly/8mepd7#https://www.nytimes.com/2021/02/21/sp...

JadeNB 6y ago
Wrong thread?
- mckirk 6y ago
  No, it's probably just a good idea to remind people of this feat, similarly to the legendary wrestling match in nineteen ninety-eight when The Undertaker threw Mankind off Hell In A Cell and plummeted 16 ft through an announcer's table.

schoen 6y ago

A game to try this out (by Kevin Buzzard, who is participating in this thread and is also the author of this blog post). https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam... I loved it and have been trying to make some subsequent levels about divisibility.

uyt 6y ago
I played it recently. I spent almost a full day to finish all the worlds and then lost interest afterwards. I think I had expectations that it would be a lot less ... tedious? Like I was hoping it would be mostly automated except needing hints whenever it got stuck. Much like how the flavor text would hint to you (the human) that you needed to use certain theorems for certain levels. Instead, it was so low level that you had to do every step of algebra manually with a line of code each. (and to be fair, in the beginning it was necessary because you're developing the usual rules of algebra as you go, but even in the later levels after they tell you about the ring tactic there's still a lot of manual algebra you need to do) The search space seems small enough that even I was just mindlessly spamming rewrite/intro/apply/induction. Why can't a computer automate this completely. And going in the other direction, I was hoping this would be a good tool to aid in proofwriting. But most of the "proof" I wrote was complete gibberish not meant for human consumption. I think the problem is because the code relies heavily on mutating a context that you can't see without using the lean UI. Anyway, maybe the number game is just not a good intro to the full capabilities of lean and I am missing the point.
- ahelwer 6y ago
  No, I think you have a pretty good grasp of things. In the real world people do use more powerful tactics like ring to skip all the low-level algebraic manipulation (which I personally really enjoyed but can see others finding tedious). Your point about proof readability applies to interactive theorem provers generally. You can see a tradeoff here between Lean/Coq and more "literate" formal proof languages like TLA+, which has a prover called TLAPS (TLA+ Proof System). TLA+ proofs are written in a hierarchical style Lamport proposed in his paper How to Write a 21st Century Proof[0], and are readable by themselves. The BIG BIG tradeoff here is that when you're writing the proof in TLA+, it's very difficult to know what the prover is "thinking" and why it is stuck. Whereas with interactive provers you know exactly what the prover is "thinking" - the proof consists solely of instructions to manipulate those thoughts which you see on screen at all times! So at this time it seems there's a tradeoff between ease of writing a formal proof and ease of reading a formal proof. [0] https://www.microsoft.com/en-us/research/publication/write-21st-century-proof/ https://www.microsoft.com/en-us/research/publication/write-2...

zant 6y ago

I absolutely love everything about this. Specially how it can provide access to knowledge to people all around the world. I'm currently thinking about getting a degree in Maths, and I find extremely appealing the notion of having a repo of knowledge from where to gather theorems, specially useful for newer developed areas.

breck 6y ago

I will pay $3.14 to the first person that formalizes mathematics using only https://treenotation.org/ https://treenotation.org/.

drdeca 6y ago
This appears to just be saying “using python style indentation to represent trees”? I don’t understand the significance. Like, yeah, you can express whatever tree you want that way. Plenty of other ways to represent trees. It’s a nice enough default if you don’t know anything about the sort of thing the tree will contain. But there’s a reason that when writing conditionals, we don’t put each symbol in the expression on their own line. Those also have their own tree structure, they are also part of the AST, but we put many of the nodes on the same line for ease of reading and editing.
- breck 6y ago
  > But there’s a reason that when writing conditionals, we don’t put one symbol in the expression on their own line I won't disagree with you. However when you zoom out and crunch the numbers, you'll find that although there are infinite expressions to put in conditionals, in practice an absolutely minuscule amount of those patterns are actually used. Context free grammars are not free. Better ways are coming.

carapace 6y ago

The only major problem (IMO) is that Lean and the others (Coq, Hol, Isabelle, Agda, Idris, etc...) are all pretty hard to read. Check out "Automated Propositional Sequent Proofs in Your Browser with Tau Prolog" for a promising approach: https://www.philipzucker.com/javascript-automated-proving/ https://www.philipzucker.com/javascript-automated-proving/ It's rendering LaTeX proof trees.

nynox 6y ago
Following this proof tree idea, this recent paper https://arxiv.org/abs/2102.03044 https://arxiv.org/abs/2102.03044 suggests to think of proofs of theorems as large trees, a tiny subset of which needs to be made explicit to convey the confidence the rest could be written out (if ever needed).
- carapace 6y ago
  Does that presuppose that it's computationally expensive to verify proofs? If so, isn't that kind of unrealistic?
  - nynox 6y ago
    Verifying fully formalized proofs is cheap. What is expensive is to produce such formalized proofs. More precisely, to formalize a proof written in a typical math paper is extremely time-consuming and not so informative (that's why it's almost never done in practice).
    - carapace 6y ago
      Ah, cheers. :) But doesn't that bring us full-circle to Buzzard's point? Isn't that why he's saying, "Hey gang, let's do math with machines." in the first place?
asdftemp 6y ago
that is a neat demo with a lot of useful links! In fact, it seems that the Lean developers/community are very interested in new methods of achieving readability, and providing users with tools to build interfaces that scale up to the complexity of real workflows. For example, Lean in vscode supports interactive html "widgets": https://youtu.be/8NUBQEZYuis?t=453 https://youtu.be/8NUBQEZYuis?t=453 (at that timestamp, there's a quick introduction to their typical use at the moment). lean4 is committed to all sorts of extensibility; here's a demonstration of the new macros: https://twitter.com/derKha/status/1354082976456441861 https://twitter.com/derKha/status/1354082976456441861. There have also been several instances of users implementing old lean3 features (for example, the `calc` tactic mode, which has unique syntax for proving (in)equalities) by simply defining new type classes and short macros.

bsdz 6y ago

Last month Kevin Buzzard gave an interesting talk "How do you convince mathematicians a theory prover is worth their time?" about how he became involved with LEAN and some of the proofs he formalised with it: https://youtu.be/8PLrxAfmC_o https://youtu.be/8PLrxAfmC_o

deleted 6y ago
[deleted]
infogulch 6y ago
During Q&A there was a friendly quarrel about 'mainstream' vs 'constructive' maths. I think there's a funny analogy in here, if you let: mainstream proof : constructive proof :: program code : machine code then Kevin is arguing that the idea of actually compiling his beautiful algorithms into machine code is silly, and that compiling program code in general is rather pointless.

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 ago
Yes, 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.

317070 6y ago

> However, AI works best with a database — and those databases are not yet there. They do, but I would tell you that if that is your main motivation to create those databases, don't do it. The AI might spend milliseconds on work that takes man-years to compile, but get stuck on absolutely tiny issues of details it can't grok and which you can quickly explain. If AI is the goal, I would propose to discuss with AI-researchers in the area of automated maths about what they can actually use to make progress. There are ways to have the AI learn unsupervised as much as possible, and to have it ask for supervision where needed. In a similar way, it took a while to teach alphaGo to play go, but it only took a couple of extra years to have alphaZero play both go and chess without any database of example games. I fully agree with the rest of the argument and I love the work that is being done to double check mathematics. But as AI researcher, I think this is a poor motivation and would warn against using it, as it might be very disappointing in the long run about how little of it turned out to be useful for AI.

voxl 6y ago
If you read the article you can tell that AI is not the goal, it is a byproduct of the goal. The goal is to have confidence in the correctness of mathematical results proved by other experts. Also, there has _already_ been some success on using AI to find proofs in lean.
_ouml_ 6y ago
There is a very active community around Lean ranging from mathematicians with no clue about computers to AI researchers trying to improve the automation. These AI researchers have explicitly said that bigger training sets will be very helpful. But like the sibling comment says, AI is not the main point.

btilly 6y ago

If anyone wants of a concrete reason to formalize mathematics, consider this. The classification of finite simple groups is a major result in mathematics that is a foundation for many others. See https://en.wikipedia.org/wiki/Classification_of_finite_simple_groups https://en.wikipedia.org/wiki/Classification_of_finite_simpl... for more. However at the time the proof was finishing, people were leaving the field, and the very people who proved it did not feel that their results were checked. They were not confident of the result. And nobody has been able to review the proof. This began a decades long effort, which is currently incomplete, to produce a second proof that is more understandable. That effort seems to have fizzled out. So one of the most important results in mathematics in the 20th century does not have a proof that anyone can understand or review. And this is true despite a number of very smart people devoting their entire lives to the subject. I maintain that no amount of human verification and re-verification will result in my being as confident of this result as I am about most mathematical results that I know. The only way to actually make this into something we should be confident of is to translate the existing proofs to something computer checkable.

edanm 6y ago
> I maintain that no amount of human verification and re-verification will result in my being as confident of this result as I am about most mathematical results that I know. The only way to actually make this into something we should be confident of is to translate the existing proofs to something computer checkable. Or to indeed find that simpler proof, I suppose? (Not disagreeing with anything you're saying, just checking - it's a fascinating story that I didn't know about this topic)
- schoen 6y ago
  I don't understand this area well at all, but I know the existing classification of finite simple groups is very long and detailed. Wikipedia says > The proof consists of tens of thousands of pages in several hundred journal articles and that the second-generation simplified version might possibly run to only 5,000 pages. 5,000 pages of math is easier to understand and/or believe in than tens of thousands of pages, but it's still a pretty daunting amount even for specialists.