[pfdietz]

I want to see a system that automates formalization of the existing math literature. LLMs are supposed to be good on language, right? So get them to read math papers and fill in the blanks, spitting out formalized versions of the results in Lean. We have centuries of literature to process, and when we're done there will be all of mathematics formalized to serve as training data for theorem provers moving into new mathematics.

[ijustlovemath]

The big problem with this is that many domains of math use hyper specialized notation, novel terms, different styles etc, and there's not much data for them to train on within any given niche.

For example, the IUT "proof" of the abc conjecture used completely novel systems to come to its conclusions, to the point that it took top number theorists a few years to even parse what it was saying, and only then could they find the faults in the proof.

I think the IUT proof would be a great adversarial example for any of these systems; if you can find the problem in the proof, you know you've hit on something pretty powerful.

[staunton]

> if you can find the problem in the proof

Is it still open whether there is a problem?

Last I heard about this, there was one guy saying there's problems and the author dismissing that as "they just didn't understand it" without showing much interest in explaining it better...

[jcla1]

I recon the general cosensus among mathematicians (as that is what counts) is that the ABC conjecture so far has _not_ been proven. Mochizuki (and his school around him) seem to be the majority of people that believe his proof is correct. As you point out, Scholze has identified a supposed flaw in Mochizuki's argument, but anyone not already at the forefront of IUT/NT/ABC conjecture is probably incapable of telling if this flaw is a true flaw or not. As Mochizuki refuses to elaborate (on this supposed flaw) consensus cannot be reached and thus the ABC conjecture remains open.

[pfdietz]

Given his behavior, I wouldn't believe anything from that guy unless it came with a formalized proof.

[staunton]

If you mistrust authors and can't actually rule out someone trying to cheat, checking a formaized proof beyond a reasonable doubt is still a lot of work and needs a huge amount of domain-specific knowledge. An author trying to cheat would try to make everything chaotic and hard to read, as well as hiding subtle flaws in theorem statements.