Gavin Leech and Václav Rozhoň are establishing a journal to review AI-generated proofs after AI solved 18 Erdős Problems

Please pass this around to anyone who would be interested:

https://docs.google.com/document/d/1P65i6o26ZyyAGefxWbhrHZChzTfutsjoxMSySEaIWBI/edit?tab=t.0#heading=h.770y9mwnk3ua

@gleech @aryehazan - any suggestions?

@gleech The Erdos problems site (+ AI wiki you link to) is in fact (implicitly) running some preliminary/experimental version of this. The tentative conclusion, at least from me, is that scaling it is *too early*. And yes, there are a lot of "cranks", where cranks here don't mean (1/n)

@gleech obvious nonsense anymore but results produced with insufficient care and/or knowledge which can be very difficult to make use of. I'd advise waiting until AI is broadly more capable, but your call. (2/n)

@gleech Note that "autoformalization" here in particular is more risky than you'd expect - you may get a lot of incomplete or partial formalizations. (3/n)

@davidmanheim @gleech I’ll be happy to consider it

I’ve been doing intensive ai theorem proving for over a year

happy to chat

@gleech I'd suggest careful human review at every step, more than you seem to be aware of, which does seem to defeat the purpose. Hence my suggestion. (4/4)