6 ms·

If I’m not mistaken, this is the first use of a proof assistant to settle the status of a difficult proof that had been sitting in limbo for years. There were s

If I’m not mistaken, this is the first use of a proof assistant to settle the status of a difficult proof that had been sitting in limbo for years. There were some previous projects (e.g. the Four Color Theorem in Coq) that validated existing proofs with a large computational element handled by untrusted software, but I think this is the first one where the epistemological status of the result was uncertain in the larger mathematical community.

isaacfrond 2y ago
Next up the abc-conjecture! Claimed to be proven in 2012, and to 400+ page paper is online. But I don't many accept the proof.
- nicklecompte 2y ago
  There is a major difference though: Holmes's proof was broadly comprehensible, just extremely complicated and easy to get lost in the details. In particular Holmes really tries to make the reader understand, with a fairly gentle/apologetic introduction. But Mochizuki's "proof" is completely impenetrable even to experts on, like, page 3, and makes no effort to explain what is happening. Another key difference is that New Foundations is a niche field, so there simply was not a huge amount of human effort spent reading Holmes's work. That's not the case with Mochizuki's proof. There's a big difference between "a small number of mathematicians didn't understand the proof but suspect it's correct" and "a large number of mathematicians didn't understand the proof and concluded it was incorrect." And, most of all: Holmes's formulation of twisted type theory made the proof a natural candidate for dependently-typed formal verification. Mochizuki's proof is not type-theoretic and does not seem like a great candidate for the calculus of constructions - maybe it is! I actually have no idea. I suspect Mochizuki is the only person in the world who can answer that. But it's critical that Holmes did so much background work to simplify his proof and make this Lean program possible. Mochizuki should do the same. AFAICT, both in terms of the "sociology of mathematics" and the amount of work required to even attempt a Lean formalization, trying to verify Mochizuki's proof is a waste of time.
  - Ericson2314 2y ago
    > And, most of all: Holmes's formulation of twisted type theory made the proof a natural candidate for dependently-typed formal verification. I am not so sure about this, actually. "twisted type theory" looks like type theory more in the original Bertrand Russel sense than in the modern (Martin Loef, Jean-Yves Girard, etc.) sense.
  - alreadydone 2y ago
    I think TTT stands for "tangled type theory".
    - randallholmes 2y ago
      It does, but I rather like "twisted type theory" :-)
    - nicklecompte 2y ago
      Oops! Good catch. I'm not an expert - I read "tangled type theory" once and "TTT" about 75 times....
  - ducttapecrown 2y ago
    Kirti Joshi from the IAS has made very serious attempts to patch up Mochizuki's work by developing new math and by making the exposition good. If you're an expert in arithmetic geometry presumably he's readable, if you're just interested, I found it fun to skim.
    - alreadydone 2y ago
      Latest update here: https://www.math.columbia.edu/~woit/wordpress/?p=13895 https://www.math.columbia.edu/~woit/wordpress/?p=13895 Unfortunately it seems Mochizuki and Scholze reached consensus that a part of Joshi's argument cannot possibly work.
    - Davidzheng 2y ago
      No comments on the correctness of his work (plenty of discussions online e.g on MO) but why do you say he's from IAS?
- nextaccountic 2y ago
  There's a proposed proof of abc conjecture that is supposedly more readable. Here is a discussion thread about it: https://www.reddit.com/r/math/comments/1bhiz0s/construction_of_arithmetic_teichmuller_spaces_iv/ https://www.reddit.com/r/math/comments/1bhiz0s/construction_... It would be nice if this one were formalized in Lean (or Coq or HOL) though.
- barfbagginus 2y ago
  I seriously doubt mochi's going to be any help for the lean formalization effort. But a lean-assistive llm trained on mochi's work? Ahhh! What an intriguing possibility!
  - Chinjut 2y ago
    I do not imagine LLMs will be of any use here.
    - barfbagginus 2y ago
      Then it's time to update your LLM reading! https://leandojo.org/ https://leandojo.org/ https://github.com/lean-dojo/LeanCopilot https://github.com/lean-dojo/LeanCopilot https://arxiv.org/abs/2404.07382 https://arxiv.org/abs/2404.07382
      - Davidzheng 2y ago
        These llm's are usually only proving some trivial lemmas right now. Hopefully it changes soon but...
        barfbagginus 2y ago
        Just bolting llms onto proof search improves the state of the art. So if you want to improve the state of the art of proof search, bolt some llms onto proof search, and enjoy! As far as making LLMs understand mochi math... I'm going to go out on a limb and say it will probably take less time for us to build an AI that understands mochi than it would take to understand mochi ourselves.
        dimask 2y ago
        I would bet for this use case LLMs to be worse than random walk, as they would probably disregard certain possibilities in crucial steps, unless we are talking about easier stuff.
- toneman 2y ago
  I have studied IUT since 2012, and it is indeed, totally baroque. However, Motizuki Theory, is totally rebased and admits results of much interest. I will write more on this matter if my claim is of mutual interest. IRT, the topic and digression here, LLM and LEAN4 are of not much use for IUT. IUT Theory is much easier understood by a hacker than by a math guy, eventually tho, monitors and tv's did kinda become the same thing but there are, some minor differences.
hiker 2y ago
Liquid Tensor Experiment also comes to mind: https://www.nature.com/articles/d41586-021-01627-2 https://www.nature.com/articles/d41586-021-01627-2 https://leanprover-community.github.io/blog/posts/lte-final/ https://leanprover-community.github.io/blog/posts/lte-final/
- Davidzheng 2y ago
  Disagree. That one was not in question for years. Only Peter Scholze proved it and said he's not completely sure
OscarCunningham 2y ago
It's a similar situation to the Kepler Conjecture (https://en.m.wikipedia.org/wiki/Kepler_conjecture https://en.m.wikipedia.org/wiki/Kepler_conjecture). The proof was already known, but people weren't sure it was correct until it was formalised.

isaacfrond 2y ago

Next up the abc-conjecture! Claimed to be proven in 2012, and to 400+ page paper is online. But I don't many accept the proof.

nicklecompte 2y ago
There is a major difference though: Holmes's proof was broadly comprehensible, just extremely complicated and easy to get lost in the details. In particular Holmes really tries to make the reader understand, with a fairly gentle/apologetic introduction. But Mochizuki's "proof" is completely impenetrable even to experts on, like, page 3, and makes no effort to explain what is happening. Another key difference is that New Foundations is a niche field, so there simply was not a huge amount of human effort spent reading Holmes's work. That's not the case with Mochizuki's proof. There's a big difference between "a small number of mathematicians didn't understand the proof but suspect it's correct" and "a large number of mathematicians didn't understand the proof and concluded it was incorrect." And, most of all: Holmes's formulation of twisted type theory made the proof a natural candidate for dependently-typed formal verification. Mochizuki's proof is not type-theoretic and does not seem like a great candidate for the calculus of constructions - maybe it is! I actually have no idea. I suspect Mochizuki is the only person in the world who can answer that. But it's critical that Holmes did so much background work to simplify his proof and make this Lean program possible. Mochizuki should do the same. AFAICT, both in terms of the "sociology of mathematics" and the amount of work required to even attempt a Lean formalization, trying to verify Mochizuki's proof is a waste of time.
- Ericson2314 2y ago
  > And, most of all: Holmes's formulation of twisted type theory made the proof a natural candidate for dependently-typed formal verification. I am not so sure about this, actually. "twisted type theory" looks like type theory more in the original Bertrand Russel sense than in the modern (Martin Loef, Jean-Yves Girard, etc.) sense.
- alreadydone 2y ago
  I think TTT stands for "tangled type theory".
  - randallholmes 2y ago
    It does, but I rather like "twisted type theory" :-)
  - nicklecompte 2y ago
    Oops! Good catch. I'm not an expert - I read "tangled type theory" once and "TTT" about 75 times....
- ducttapecrown 2y ago
  Kirti Joshi from the IAS has made very serious attempts to patch up Mochizuki's work by developing new math and by making the exposition good. If you're an expert in arithmetic geometry presumably he's readable, if you're just interested, I found it fun to skim.
  - alreadydone 2y ago
    Latest update here: https://www.math.columbia.edu/~woit/wordpress/?p=13895 https://www.math.columbia.edu/~woit/wordpress/?p=13895 Unfortunately it seems Mochizuki and Scholze reached consensus that a part of Joshi's argument cannot possibly work.
  - Davidzheng 2y ago
    No comments on the correctness of his work (plenty of discussions online e.g on MO) but why do you say he's from IAS?
nextaccountic 2y ago
There's a proposed proof of abc conjecture that is supposedly more readable. Here is a discussion thread about it: https://www.reddit.com/r/math/comments/1bhiz0s/construction_of_arithmetic_teichmuller_spaces_iv/ https://www.reddit.com/r/math/comments/1bhiz0s/construction_... It would be nice if this one were formalized in Lean (or Coq or HOL) though.
barfbagginus 2y ago
I seriously doubt mochi's going to be any help for the lean formalization effort. But a lean-assistive llm trained on mochi's work? Ahhh! What an intriguing possibility!
- Chinjut 2y ago
  I do not imagine LLMs will be of any use here.
  - barfbagginus 2y ago
    Then it's time to update your LLM reading! https://leandojo.org/ https://leandojo.org/ https://github.com/lean-dojo/LeanCopilot https://github.com/lean-dojo/LeanCopilot https://arxiv.org/abs/2404.07382 https://arxiv.org/abs/2404.07382
    - Davidzheng 2y ago
      These llm's are usually only proving some trivial lemmas right now. Hopefully it changes soon but...
      - barfbagginus 2y ago
        Just bolting llms onto proof search improves the state of the art. So if you want to improve the state of the art of proof search, bolt some llms onto proof search, and enjoy! As far as making LLMs understand mochi math... I'm going to go out on a limb and say it will probably take less time for us to build an AI that understands mochi than it would take to understand mochi ourselves.
        dimask 2y ago
        I would bet for this use case LLMs to be worse than random walk, as they would probably disregard certain possibilities in crucial steps, unless we are talking about easier stuff.
toneman 2y ago
I have studied IUT since 2012, and it is indeed, totally baroque. However, Motizuki Theory, is totally rebased and admits results of much interest. I will write more on this matter if my claim is of mutual interest. IRT, the topic and digression here, LLM and LEAN4 are of not much use for IUT. IUT Theory is much easier understood by a hacker than by a math guy, eventually tho, monitors and tv's did kinda become the same thing but there are, some minor differences.

hiker 2y ago

Liquid Tensor Experiment also comes to mind: https://www.nature.com/articles/d41586-021-01627-2 https://www.nature.com/articles/d41586-021-01627-2 https://leanprover-community.github.io/blog/posts/lte-final/ https://leanprover-community.github.io/blog/posts/lte-final/

Davidzheng 2y ago
Disagree. That one was not in question for years. Only Peter Scholze proved it and said he's not completely sure

OscarCunningham 2y ago

It's a similar situation to the Kepler Conjecture (https://en.m.wikipedia.org/wiki/Kepler_conjecture https://en.m.wikipedia.org/wiki/Kepler_conjecture). The proof was already known, but people weren't sure it was correct until it was formalised.