guaranteed, up to lean itself having bugs that are exploited by the LLM :shrug:
Well considering the proof is pretty much accepted by mathematicians to be correct (I'll be happy with that!), it would be sort of unnecessary to cheat. Maybe if some aspect is really tricky to formalize it could have done something there? If I had to search for it, I would go for parts of the original proof that are "outsourced" to other mathematical works. Imagine one of the agents struggling to download a paper due to a paywall or whatever and just deciding to cheat lol
Do you have proof of this bug or something? Is this just envy against computers now ?