Lakatos (maybe it was Polya?) book on intuition in math provides intellectual framework for why LLMs trained with RLVR are more effective for math than AlphaProof-type formal systems Implications: 1. Maybe reasoning in continuous space is better because it more closely approximates our intuition - not limited to what can be explicitly said 2. Intuition tends to occur in large chunks that increase in resolution as more thought is given. LLMs are restricted to thinking at token level resolution. Maybe having some type of chunked representation space for the LLM to think in could even further improve intuition 3. LLM as renowned professor, AlphaProof as grad student. LLM outputs an informal sketch of the proof it arrived at through informal intuition (like a bolt of insight from a seasoned professor PhD advisor). Job of AlphaEvolve is to formalize proof sketch, while proof sketch significantly prunes search tree of AlphaEvolve. Can have a loop between them to iterate on proof sketch if formalization fails