5 ms·

Thanks for sharing. It seems there are a lot of different formalization systems. (11 listed on this site). It seems strange to me that there isn't one standar

Thanks for sharing. It seems there are a lot of different formalization systems. (11 listed on this site). It seems strange to me that there isn't one standard system. I don't know much about modern mathematics. But seems odd to me there isn't more of a movement to formalise all proofs. And to get computers / AI involved in discovering new proofs. Please some explain to me! (I have lots of ignorance of these things)

tromp 3y ago
> It seems strange to me that there isn't one standard system. It would be much stranger to me if there was only one. These formal systems are much like programming languages, and just like those, come in many flavors, appealing to different appetites. Where programming languages can be based on procedures, objects, or functions, proof systems can be based on set theory, on simple type theory, or on dependent type theory. In his comparison of formal systems [1], Freek Wiedijk identifies no less than seven ways to represent mathematics. [1] https://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf https://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf
- riku_iki 3y ago
  > These formal systems are much like programming languages, and just like those, come in many flavors, appealing to different appetites. and they all compile into the same fol/hol assembly (e.g. Isabelle translates its languages to fol and uses E for actual theorem proving, and E knows nothing about Isabelle language coolness), so in theory they should be able to integrate nicely. My understanding is that the problem is they formalize in different mathematical foundations/axiomatic theories, but I am not an expert in this.
  - carnitine 3y ago
    They definitely don’t all compile to the same thing. Some do, most don’t.
    - riku_iki 3y ago
      I meant to say they are all the same thing on logical level, all those fancy typed theories can be reduced to hol/fol, for some it is implemented, for others not.
      - carnitine 3y ago
        That’s not true either. Coq’s logic is significantly different to HoL.
        riku_iki 3y ago
        hol meaning higher order logic (https://en.wikipedia.org/wiki/Higher-order_logic https://en.wikipedia.org/wiki/Higher-order_logic) not the lang of hol prover.
infruset 3y ago
I've seen the same reaction from people learning to program. Why are there thousands of programming languages? Why not put everything under one standard? The main answer, as for many variations of this question (languages, laws, units of measure, programming languages), is history. Efforts to formalize mathematics have spawned in different universities, at different times, in different teams with different cultures and approaches. The mathematical theories underlying the software also vary greatly. There isn't one agreed upon formalization of mathematics. There's classical logic and there's intuitionistic logic, which wants to see every existence theorem backed by an actual witness and does not agree that `not (not A) = A`. (Speaking of which, different systems have (very) different notions of equality! In case you thought this one would at least be simple). Sometimes two pieces of software have nearly identical foundations, such as Lean and Coq to some extent; but one is decades old, and the other is a rewrite from scratch using other unification algorithms and a different programming language. Sometimes people just don't get along and start competing projects. Note that some people have intended to unify various proof systems, which reminds me of the classical https://xkcd.com/927/ https://xkcd.com/927/
Certhas 3y ago
Not an expert, but I think your question is roughly analogous to asking why there isn't one programming language. There are many different approaches to writing formalization systems, and so far we don't have one that has won out as clearly superior (though from the outside it looks like Lean has the most momentum, and is the only one that has been used on cutting edge mathematics as far as I know). On your question why there isn't more of a movement to formalize proofs: Proofs as written are for communicating and convincing other humans. Humans are _very_ good at filling in gaps. You can say things like: "In what follows we need this minor property to hold, it can be proven easily using Properties 4, 5, and 6 established above by using the strategy X". Here easily means "easy for a specialist who has dedicated 10 years to study this stuff", which is the target audience for your writing. If you instead need to explain this minor result to a formalization engine, you have to spell out every. single. last. detail. That's tedious and it adds very little rigor. https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/Y022904/1 https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/Y0... Kevin Buzzard got a 5 year grant to get started on formalizing the proof of Fermats Last Theorem. Thats the amount of extra effort we are talking.
- Pet_Ant 3y ago
  > Kevin Buzzard got a 5 year grant to get started on formalizing the proof of Fermats Last Theorem. Thats the amount of extra effort we are talking. Wouldn't Andrew Wiles be the best person for it?
  - Certhas 3y ago
    The skills needed to formalize the proof and come up with the proof are probably quite distinct. There are many people now who understand the proof well. Also, even if Wiles would be the best person to do it, he might be more inclined to spend the next five years on new mathematical ideas rather than on convincing a computer program his old ideas are correct.
smatija 3y ago
I vaguely remember from my undergrad that formalising all proofs isn't possible, due to axiom of choice making some issues (and if you decide to abandon axiom of choice, like in constructive mathematics, you lose real numbers). It was a very interesting class, we mostly used Coq.
- IngoBlechschmid 3y ago
  Two tiny additions: 1. In those proof assistants which don't have the axiom of choice built-in, you can still formalize proofs depending on this axiom by putting it as an extra assumption. One repository using this style which I particularly like is the one by Martín Escardó: https://www.cs.bham.ac.uk//~mhe/TypeTopology/index.html https://www.cs.bham.ac.uk//~mhe/TypeTopology/index.html He even takes care to explicitly put axioms as visible assumptions which are almost always taken for granted, such as function extensionality. 2. You don't need the axiom of choice to construct the real numbers, in fact several constructions are available (Dedekind cuts, Cauchy sequences, Cauchy processes, ...) and all do their job. It's just that without the (countable) axiom of choice, you cannot prove that the Cauchy real numbers are complete. But the other constructions work fine even in the absence of choice.
- Gajurgensen 3y ago
  Coq is constructive be default, but you can add the axiom of choice and the law of the excluded middle to make it classical (other common axioms are functional extensionality, propositional extensionality, and proof irrelevance). Perhaps you are recalling Godel's incompleteness theorem, which says that for any finite formal system (like Coq) there exists a true theorem it is unable to prove?
contravariant 3y ago
> But seems odd to me there isn't more of a movement to formalise all proofs. Well, from the perspective of mathematicians all known proofs are formalized by definition (to some extent anyway). Putting them through a proof checker is not completely without merit, but is not exactly highest priority. As for discovering new proofs, it's a bit tricky to tell a computer what to find interesting. And the reasoning behind a proof is often more important than the exact steps themselves.
IngoBlechschmid 3y ago
Good questions! Nowadays, there is indeed a movement towards interoperability between the various proof assistants, one of these bridge-building projects is called Dedukti: https://deducteam.github.io/ https://deducteam.github.io/ It's a challenging project because the different proof assistants which are currently in use differ in their foundational perspectives and their idioms. The question how to best formalize mathematics is still an open research problem, just as the question how to best develop programs, but we already have quite a good understanding of many important issues in this area. Also, by now there are attempts to use AI for discovering proofs, see for instance https://leandojo.org/ https://leandojo.org/ or https://github.com/lean-dojo/LeanDojoChatGPT https://github.com/lean-dojo/LeanDojoChatGPT.
Gajurgensen 3y ago
Theorem provers aren't just for mathematicians formalizing mathematics. Although, for that purpose, Lean seems to be very popular these days (perhaps followed by Coq?). Theorem provers are also used to formalize software and hardware systems. The people using theorem provers are diverse in their tasks and priorities. Consider three provers/languages: Coq, ACL2, and Dafny. Coq is a very expressive, dependently-typed, higher-order functional language, much in the spirit of Haskell or SML. It is very powerful for writing specifications due to this expressivity, and is therefore a compelling candidate for formalizing mathematics. It also has a very clean separation between proof search and proof checking, allowing for a smaller trusted kernel in the proof checker. However, due to the complexity of the language, writing proofs tends to be a largely manual task, or require domain-specific automation. ACL2, on the other hand, is simpler in its language. It is a first order logic, built atop a total, untyped (at least logically) lisp. It does not produce proof artifacts like Coq, but proofs are much more automated, consisting of only a handful of hints instead of an entire tactic-tree. Finally, Dafny is an imperative language, very much resembling popular and ubiquitous languages familiar to every programmer. Proofs are managed by adding inline annotations, specifying pre and postconditions, invariants, etc. This does not expose hardly any of the proof internals, and may be difficult for large proofs, but is a relatively friendly interface for the working software engineer.
BeetleB 3y ago
> I don't know much about modern mathematics. But seems odd to me there isn't more of a movement to formalise all proofs. Only a tiny percentage of mathematicians use such systems. Historically they arose from CS, not math, so most mathematicians aren't trained in it. And until recently, the two camps spoke different languages (i.e. different terminology for the same concept), so there was a barrier for a given mathematician to learn, say, Coq. It's also very time consuming. A proof a mathematician can write down in 10 minutes may take him a day to formalize in a proof assistant. Still, things are changing, and more mathematicians are toying with them. You can see Terence Tao experimenting with Lean on his Mastodon account: https://mathstodon.xyz/@tao https://mathstodon.xyz/@tao

tromp 3y ago

> It seems strange to me that there isn't one standard system. It would be much stranger to me if there was only one. These formal systems are much like programming languages, and just like those, come in many flavors, appealing to different appetites. Where programming languages can be based on procedures, objects, or functions, proof systems can be based on set theory, on simple type theory, or on dependent type theory. In his comparison of formal systems [1], Freek Wiedijk identifies no less than seven ways to represent mathematics. [1] https://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf https://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf

riku_iki 3y ago
> These formal systems are much like programming languages, and just like those, come in many flavors, appealing to different appetites. and they all compile into the same fol/hol assembly (e.g. Isabelle translates its languages to fol and uses E for actual theorem proving, and E knows nothing about Isabelle language coolness), so in theory they should be able to integrate nicely. My understanding is that the problem is they formalize in different mathematical foundations/axiomatic theories, but I am not an expert in this.
- carnitine 3y ago
  They definitely don’t all compile to the same thing. Some do, most don’t.
  - riku_iki 3y ago
    I meant to say they are all the same thing on logical level, all those fancy typed theories can be reduced to hol/fol, for some it is implemented, for others not.
    - carnitine 3y ago
      That’s not true either. Coq’s logic is significantly different to HoL.
      - riku_iki 3y ago
        hol meaning higher order logic (https://en.wikipedia.org/wiki/Higher-order_logic https://en.wikipedia.org/wiki/Higher-order_logic) not the lang of hol prover.

infruset 3y ago

I've seen the same reaction from people learning to program. Why are there thousands of programming languages? Why not put everything under one standard? The main answer, as for many variations of this question (languages, laws, units of measure, programming languages), is history. Efforts to formalize mathematics have spawned in different universities, at different times, in different teams with different cultures and approaches. The mathematical theories underlying the software also vary greatly. There isn't one agreed upon formalization of mathematics. There's classical logic and there's intuitionistic logic, which wants to see every existence theorem backed by an actual witness and does not agree that `not (not A) = A`. (Speaking of which, different systems have (very) different notions of equality! In case you thought this one would at least be simple). Sometimes two pieces of software have nearly identical foundations, such as Lean and Coq to some extent; but one is decades old, and the other is a rewrite from scratch using other unification algorithms and a different programming language. Sometimes people just don't get along and start competing projects. Note that some people have intended to unify various proof systems, which reminds me of the classical https://xkcd.com/927/ https://xkcd.com/927/

Certhas 3y ago

Not an expert, but I think your question is roughly analogous to asking why there isn't one programming language. There are many different approaches to writing formalization systems, and so far we don't have one that has won out as clearly superior (though from the outside it looks like Lean has the most momentum, and is the only one that has been used on cutting edge mathematics as far as I know). On your question why there isn't more of a movement to formalize proofs: Proofs as written are for communicating and convincing other humans. Humans are _very_ good at filling in gaps. You can say things like: "In what follows we need this minor property to hold, it can be proven easily using Properties 4, 5, and 6 established above by using the strategy X". Here easily means "easy for a specialist who has dedicated 10 years to study this stuff", which is the target audience for your writing. If you instead need to explain this minor result to a formalization engine, you have to spell out every. single. last. detail. That's tedious and it adds very little rigor. https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/Y022904/1 https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/Y0... Kevin Buzzard got a 5 year grant to get started on formalizing the proof of Fermats Last Theorem. Thats the amount of extra effort we are talking.

Pet_Ant 3y ago
> Kevin Buzzard got a 5 year grant to get started on formalizing the proof of Fermats Last Theorem. Thats the amount of extra effort we are talking. Wouldn't Andrew Wiles be the best person for it?
- Certhas 3y ago
  The skills needed to formalize the proof and come up with the proof are probably quite distinct. There are many people now who understand the proof well. Also, even if Wiles would be the best person to do it, he might be more inclined to spend the next five years on new mathematical ideas rather than on convincing a computer program his old ideas are correct.

smatija 3y ago

I vaguely remember from my undergrad that formalising all proofs isn't possible, due to axiom of choice making some issues (and if you decide to abandon axiom of choice, like in constructive mathematics, you lose real numbers). It was a very interesting class, we mostly used Coq.

IngoBlechschmid 3y ago
Two tiny additions: 1. In those proof assistants which don't have the axiom of choice built-in, you can still formalize proofs depending on this axiom by putting it as an extra assumption. One repository using this style which I particularly like is the one by Martín Escardó: https://www.cs.bham.ac.uk//~mhe/TypeTopology/index.html https://www.cs.bham.ac.uk//~mhe/TypeTopology/index.html He even takes care to explicitly put axioms as visible assumptions which are almost always taken for granted, such as function extensionality. 2. You don't need the axiom of choice to construct the real numbers, in fact several constructions are available (Dedekind cuts, Cauchy sequences, Cauchy processes, ...) and all do their job. It's just that without the (countable) axiom of choice, you cannot prove that the Cauchy real numbers are complete. But the other constructions work fine even in the absence of choice.
Gajurgensen 3y ago
Coq is constructive be default, but you can add the axiom of choice and the law of the excluded middle to make it classical (other common axioms are functional extensionality, propositional extensionality, and proof irrelevance). Perhaps you are recalling Godel's incompleteness theorem, which says that for any finite formal system (like Coq) there exists a true theorem it is unable to prove?

contravariant 3y ago

> But seems odd to me there isn't more of a movement to formalise all proofs. Well, from the perspective of mathematicians all known proofs are formalized by definition (to some extent anyway). Putting them through a proof checker is not completely without merit, but is not exactly highest priority. As for discovering new proofs, it's a bit tricky to tell a computer what to find interesting. And the reasoning behind a proof is often more important than the exact steps themselves.

IngoBlechschmid 3y ago

Good questions! Nowadays, there is indeed a movement towards interoperability between the various proof assistants, one of these bridge-building projects is called Dedukti: https://deducteam.github.io/ https://deducteam.github.io/ It's a challenging project because the different proof assistants which are currently in use differ in their foundational perspectives and their idioms. The question how to best formalize mathematics is still an open research problem, just as the question how to best develop programs, but we already have quite a good understanding of many important issues in this area. Also, by now there are attempts to use AI for discovering proofs, see for instance https://leandojo.org/ https://leandojo.org/ or https://github.com/lean-dojo/LeanDojoChatGPT https://github.com/lean-dojo/LeanDojoChatGPT.

Gajurgensen 3y ago

Theorem provers aren't just for mathematicians formalizing mathematics. Although, for that purpose, Lean seems to be very popular these days (perhaps followed by Coq?). Theorem provers are also used to formalize software and hardware systems. The people using theorem provers are diverse in their tasks and priorities. Consider three provers/languages: Coq, ACL2, and Dafny. Coq is a very expressive, dependently-typed, higher-order functional language, much in the spirit of Haskell or SML. It is very powerful for writing specifications due to this expressivity, and is therefore a compelling candidate for formalizing mathematics. It also has a very clean separation between proof search and proof checking, allowing for a smaller trusted kernel in the proof checker. However, due to the complexity of the language, writing proofs tends to be a largely manual task, or require domain-specific automation. ACL2, on the other hand, is simpler in its language. It is a first order logic, built atop a total, untyped (at least logically) lisp. It does not produce proof artifacts like Coq, but proofs are much more automated, consisting of only a handful of hints instead of an entire tactic-tree. Finally, Dafny is an imperative language, very much resembling popular and ubiquitous languages familiar to every programmer. Proofs are managed by adding inline annotations, specifying pre and postconditions, invariants, etc. This does not expose hardly any of the proof internals, and may be difficult for large proofs, but is a relatively friendly interface for the working software engineer.

BeetleB 3y ago

> I don't know much about modern mathematics. But seems odd to me there isn't more of a movement to formalise all proofs. Only a tiny percentage of mathematicians use such systems. Historically they arose from CS, not math, so most mathematicians aren't trained in it. And until recently, the two camps spoke different languages (i.e. different terminology for the same concept), so there was a barrier for a given mathematician to learn, say, Coq. It's also very time consuming. A proof a mathematician can write down in 10 minutes may take him a day to formalize in a proof assistant. Still, things are changing, and more mathematicians are toying with them. You can see Terence Tao experimenting with Lean on his Mastodon account: https://mathstodon.xyz/@tao https://mathstodon.xyz/@tao