Hacker News Reader

You are a human, not an AI. You know whether your idea seems related to the solution. The AI has thousands of ideas and doesn't know which are better. Graders shouldn't accept a thousand guesses grubbing for 1 point.

If verifying a good idea is easy, then the evidence shows that the AI didn't have good ideas for the other 2 problems.

View on HN

we are talking about lean proofs. Given a formal statement and a proof - the lean can verify whether it's correct or not. It's like generating computer programs to solve a problem - the problem lied in generating useful solutions/sub-solutions so that the search is effective. They achieve this via using gemini as a lean proof generator aka. using a world model LLM fine tuned to generate lean proofs in a more effective manner.

Humans are even better at this as you mention - but effectively the approach is similar. Come up with lot of ideas and see what proves it.

Reply on news.ycombinator.com