5 ms·

Formalizing 100 Theorems

66 points by bindidwodtj 3y ago

matthewfelgate 3y ago
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
Out of these 100 famous theorems, only 33. Fermat's Last Theorem has yet to be proven in a formal system. It's like Formal's Last Theorem :-)
- matthewfelgate 3y ago
  LOL
- pitdicker 3y ago
  Good look to whomever is going to formalize that! Does anyone have an idea of the amount of effort it would take? Would the effort be comparable with the original proof by Andrew Wiles?
  - mazsa 3y ago
    "Here is a list of some of what has been written about this or things we can do:" https://github.com/metamath/set.mm/wiki/Fermat's-Last-Theorem https://github.com/metamath/set.mm/wiki/Fermat's-Last-Theore...
  - dvh 3y ago
    If HN had slightly wider margin it could easily fit there.
    - hansbcarlsen 3y ago
      i rarely comment here.
  - kevinwang 3y ago
    Apparently a few years: https://x.com/XenaProject/status/1712488019016515662?s=20 https://x.com/XenaProject/status/1712488019016515662?s=20
- muldvarp 3y ago
  Prof. Kevin Buzzard got a research grant for formalizing FLT in Lean. https://twitter.com/XenaProject/status/1712488019016515662 https://twitter.com/XenaProject/status/1712488019016515662
gosub100 3y ago
Theorem proving is something I'm curious about. Can someone familiar explain why it's difficult, say, in an imperative language, to represent mathematical notation? I'm not saying its impossible, but why can't you start from 0 = 0, and apply random permutations with symbols on either side, check them for truth, discard the junk, and eventually arrive at the quadratic formula? Or a step further, derive (by randomly applying logical rules) the infinitely-many-primes theorem? Essentially, why can't you just trade CPU cycles for logical proofs and equations? What reading can you recommend that bridges (or addresses) programming language theory (BNF grammars, etc) to mathematics?
- markusde 3y ago
  A problem with randomly searching for theorems is that it blows up exponentially, and many of the theorems you would find are probably not useful in their own right. Another problem is that "check the for truth" is undecidable: they are what I think of when you mention "trade CPU cycles for proofs" though if you're just trying to prove random theorems they will be limited.
  - jerf 3y ago
    "many of the theorems you would find are probably not useful in their own right" To give an example, there's an infinite array of "If X is greater than 20, X is greater than 10" theorems. Obviously useless to prove each of them, but enumeration will encounter all of these, as well as a huge number of classes of similar theorems, in the process of getting to anything interesting. You can't just "skip" them either, because they get arbitrarily complicated. I chose a really simple one to drive home the point, and because it's the sort of theorem you'll hit early, but tautologies can be arbitrarily complicated. Trying to create something that identifies them hits halting problems of their own. Rice's Theorem, which can be colloquially summarized as "any interesting property is not computable", will stop you, among other things. ("If X is a prime > 521, X does not have 21 as a factor." "If X is irrational, its fraction expansion does not have a denominator between 15 and 54." "If the absolute value of X is not equal to X, X < 932." "If the fractional component of X is greater than .5, the first digit of the fraction expansion is not 2 or 4." "The sum of two positive numbers is greater than the smallest of the two numbers number minus 273,883,192,823." "Most" theorems are really, really useless.)
levn11 3y ago
https://archive.org/details/fermat-3/page/n5/mode/2up https://archive.org/details/fermat-3/page/n5/mode/2up If you would like to check out an elementary proof for Fermat's Last Theorem (or at least an attempt)
Gajurgensen 3y ago
ACL2 has a documentation page for the theorems from this list proved: https://www.cs.utexas.edu/users/moore/acl2/manuals/latest/index.html?topic=ACL2____100-THEOREMS https://www.cs.utexas.edu/users/moore/acl2/manuals/latest/in... A couple of theorems have actually been proved but not yet reported/counted.

66 points by bindidwodtj 3y ago

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

Out of these 100 famous theorems, only 33. Fermat's Last Theorem has yet to be proven in a formal system. It's like Formal's Last Theorem :-)

matthewfelgate 3y ago
LOL
pitdicker 3y ago
Good look to whomever is going to formalize that! Does anyone have an idea of the amount of effort it would take? Would the effort be comparable with the original proof by Andrew Wiles?
- mazsa 3y ago
  "Here is a list of some of what has been written about this or things we can do:" https://github.com/metamath/set.mm/wiki/Fermat's-Last-Theorem https://github.com/metamath/set.mm/wiki/Fermat's-Last-Theore...
- dvh 3y ago
  If HN had slightly wider margin it could easily fit there.
  - hansbcarlsen 3y ago
    i rarely comment here.
- kevinwang 3y ago
  Apparently a few years: https://x.com/XenaProject/status/1712488019016515662?s=20 https://x.com/XenaProject/status/1712488019016515662?s=20
muldvarp 3y ago
Prof. Kevin Buzzard got a research grant for formalizing FLT in Lean. https://twitter.com/XenaProject/status/1712488019016515662 https://twitter.com/XenaProject/status/1712488019016515662

gosub100 3y ago

Theorem proving is something I'm curious about. Can someone familiar explain why it's difficult, say, in an imperative language, to represent mathematical notation? I'm not saying its impossible, but why can't you start from 0 = 0, and apply random permutations with symbols on either side, check them for truth, discard the junk, and eventually arrive at the quadratic formula? Or a step further, derive (by randomly applying logical rules) the infinitely-many-primes theorem? Essentially, why can't you just trade CPU cycles for logical proofs and equations? What reading can you recommend that bridges (or addresses) programming language theory (BNF grammars, etc) to mathematics?

markusde 3y ago
A problem with randomly searching for theorems is that it blows up exponentially, and many of the theorems you would find are probably not useful in their own right. Another problem is that "check the for truth" is undecidable: they are what I think of when you mention "trade CPU cycles for proofs" though if you're just trying to prove random theorems they will be limited.
- jerf 3y ago
  "many of the theorems you would find are probably not useful in their own right" To give an example, there's an infinite array of "If X is greater than 20, X is greater than 10" theorems. Obviously useless to prove each of them, but enumeration will encounter all of these, as well as a huge number of classes of similar theorems, in the process of getting to anything interesting. You can't just "skip" them either, because they get arbitrarily complicated. I chose a really simple one to drive home the point, and because it's the sort of theorem you'll hit early, but tautologies can be arbitrarily complicated. Trying to create something that identifies them hits halting problems of their own. Rice's Theorem, which can be colloquially summarized as "any interesting property is not computable", will stop you, among other things. ("If X is a prime > 521, X does not have 21 as a factor." "If X is irrational, its fraction expansion does not have a denominator between 15 and 54." "If the absolute value of X is not equal to X, X < 932." "If the fractional component of X is greater than .5, the first digit of the fraction expansion is not 2 or 4." "The sum of two positive numbers is greater than the smallest of the two numbers number minus 273,883,192,823." "Most" theorems are really, really useless.)

levn11 3y ago

https://archive.org/details/fermat-3/page/n5/mode/2up https://archive.org/details/fermat-3/page/n5/mode/2up If you would like to check out an elementary proof for Fermat's Last Theorem (or at least an attempt)

Gajurgensen 3y ago

ACL2 has a documentation page for the theorems from this list proved: https://www.cs.utexas.edu/users/moore/acl2/manuals/latest/index.html?topic=ACL2____100-THEOREMS https://www.cs.utexas.edu/users/moore/acl2/manuals/latest/in... A couple of theorems have actually been proved but not yet reported/counted.