Post #1684319

Replies (1)

• @highergeometer@mathstodon.xyz 2026-04-21 05:10

  @TonyVladusich Well, Mochizuki's team is doing the responsible thing and thinking about formalisation of the core part of the argument, and an independent team is also looking at formalising a bunch of anabelian geometry to get to the point of encoding the claims - whether this shows the idea is irrecoverably flawed, or Scholze and Stix's argument with a simplified version wasn't strong enough, we will see. Scholze and Stix openly acknowledged their argument was based a stripped down picture, and they claim this still captured the essentials. People are definitely convinced by the argument, but doing it in Lean will ideally fully close the door for everyone, and at the same time, get a lot of interesting mathematics more rigorously described; the "functorial reconstruction" stuff that Mochizuki depends on is legitimate anabelian geometry that is not done that well in the literature. You can tell by the fact Mochizuki thought you *needed* to do everything in ZFC with first-order formulas, and worried about accidental loops using ∈, when really this shouldn't be necessary at all, that the mentality around these methods is not fully matured.

  Open ##1684320