3 ms·
As explained in another comment, there is only very mild proof automation going on in this Lean project. Every non-trivial idea has to be supplied to the comput
by deadbeef57 5y ago
As explained in another comment, there is only very mild proof automation going on in this Lean project. Every non-trivial idea has to be supplied to the computer by a human being.
The whole circus around Mochizuki's proof of the abc conjecture was dealt with quite well by the social structure of the mathematical community. Many people looked at the proof. Many people got stuck. Several experts got stuck at exactly the same point. And Mochizuki refuses to acknowledge that there is a problem at that point of his "proof". But a consensus was reached in the mathematical community (maybe minus RIMS).
- kungito 5y agoWhat's the name of this point? It's really hard to find any progress on this topic regarding Mochizuki other than some popular articles without any content.
- deadbeef57 5y agoSee https://www.math.columbia.edu/~woit/wordpress/?p=10560 https://www.math.columbia.edu/~woit/wordpress/?p=10560, which links to a technical write-up by Scholze and Stix about what they think is the issue with Mochizuki's proof. Woit's blogpost also gives a bit more links, including a response by Mochizuki.
- bryan0 5y agoThe paper which everyone linked to when the discussion was going on now 404s, so here is a new link: https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture.pdf https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture... The point in the proof where scholze and stix show it fails is “IUTT-3, Corollary 3.12”