[JonChesterfield]

You too can solve maths problems by:

1. Generating enormous amounts of text

2. Persuading a mathematician to look closely at it

3. Announcing success if they conclude it is a proof

This is deeply disappointing relative to "chatgpt found a proof that isabelle verifies" or similar, especially the part where a mathematician spends (presumably hours) reading through the llm output.

[booleandilemma]

I think large proofs done by humans also require hours of verification by other mathematicians, checking for "bugs" in a sense. I don't think they're obviously correct, I think it's like more like doing a code review.