@incollection{Bengio+chapter2007,
author = {Bengio, Yoshua and LeCun, Yann},
booktitle = {Large Scale Kernel Machines},
publisher = {MIT Press},
title = {Scaling Learning Algorithms Towards {AI}},
year = {2007}
}

@article{Hinton06,
author = {Hinton, Geoffrey E. and Osindero, Simon and Teh, Yee Whye},
journal = {Neural Computation},
pages = {1527--1554},
title = {A Fast Learning Algorithm for Deep Belief Nets},
volume = {18},
year = {2006}
}

@book{goodfellow2016deep,
title={Deep learning},
author={Goodfellow, Ian and Bengio, Yoshua and Courville, Aaron and Bengio, Yoshua},
volume={1},
year={2016},
publisher={MIT Press}
}


@article{poesia2024minimo,
  title={Learning formal mathematics from intrinsic motivation},
  author={Poesia, Gabriel and Broman, David and Haber, Nick and Goodman, Noah D},
  journal={Advances in Neural Information Processing Systems},
  volume={37},
  pages={43032--43057},
  year={2024}
}

@inproceedings{demoura2008z3,
  title={Z3: An efficient SMT solver},
  author={De Moura, Leonardo and Bj{\o}rner, Nikolaj},
  booktitle={International conference on Tools and Algorithms for the Construction and Analysis of Systems},
  pages={337--340},
  year={2008},
  organization={Springer}
}

@misc{openai-finite-time-blowup,
  author = {OpenAI},
  keywords = {Mathematical Physics, Fluid Dynamics, Navier–Stokes Equations, Finite Time Blowup},
  title = {Finite Time Blowup for Navier–Stokes},
  url = {https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf},
  year = {2026},
  publisher = {OpenAI}
}

@misc{dong2025stpselfplayllmtheorem,
      title={STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving}, 
      author={Kefan Dong and Tengyu Ma},
      year={2025},
      eprint={2502.00212},
      archivePrefix={arXiv},
      primaryClass={cs.LG},
      url={https://arxiv.org/abs/2502.00212}, 
}

@article{poesia2023peano,
  title={Peano: learning formal mathematical reasoning},
  author={Poesia, Gabriel and Goodman, Noah D},
  journal={Philosophical transactions. Series A, Mathematical, physical, and engineering sciences},
  volume={381},
  number={2251},
  pages={20220044},
  year={2023}
}

@article{vaswani2017attention,
  title={Attention is all you need},
  author={Vaswani, Ashish and Shazeer, Noam and Parmar, Niki and Uszkoreit, Jakob and Jones, Llion and Gomez, Aidan N and Kaiser, {\L}ukasz and Polosukhin, Illia},
  journal={Advances in neural information processing systems},
  volume={30},
  year={2017}
}

@article{johansson2011conjecture,
  title={Conjecture synthesis for inductive theories},
  author={Johansson, Moa and Dixon, Lucas and Bundy, Alan},
  journal={Journal of automated reasoning},
  volume={47},
  number={3},
  pages={251--289},
  year={2011},
  publisher={Springer}
}

@inproceedings{lenat11984automated,
author = {Lenat, Douglas B.},
title = {Automated theory formation in mathematics},
year = {1977},
publisher = {Morgan Kaufmann Publishers Inc.},
address = {San Francisco, CA, USA},
abstract = {A program called "AM" is described which cairies on simple mathematics research: defining, and studying new concepts under the guidance of a large body of heuiistic rules. The 250 heurKtus communicate via an agenda mechanism, a global priority queue of small bisk', for the program to perform and teasons why each task is plausible (e.g., "Find PENCRAHZTION. of 'prnes', because turued out to be so useful a Concept"). Each concept is an active, structured knowledge module. One bundled very incomplete modules are initially supplied, each one corresponding to an elementary set theoretic concept (e.g., union). This provides a definite but immense space which AM begins to explore. In one boor, AM rediscovers hundreds of common concepts (including singleton sets, natural numbers, arithmetic) and theorems (e.g., unique factorization).},
booktitle = {Proceedings of the 5th International Joint Conference on Artificial Intelligence - Volume 2},
pages = {833–842},
numpages = {10},
location = {Cambridge, USA},
series = {IJCAI'77}
}


@inproceedings{colton2001automated,
  title={Automated Theory Formation in Pure Mathematics},
  author={Simon Colton},
  booktitle={Distinguished dissertations},
  year={2002},
  url={https://api.semanticscholar.org/CorpusID:118130982}
}

@article{graffiti,
author = {Fajtlowicz, Siemion},
title = {On conjectures of Graffiti},
year = {1988},
issue_date = {Dec 1988},
publisher = {Elsevier Science Publishers B. V.},
address = {NLD},
volume = {72},
number = {1-3},
issn = {0012-365X},
url = {https://doi.org/10.1016/0012-365X(88)90199-9},
doi = {10.1016/0012-365X(88)90199-9},
journal = {Discrete Math.},
month = dec,
pages = {113–118},
numpages = {6}
}

@misc{bailey2026scalingselfplayselfguidance,
      title={Scaling Self-Play with Self-Guidance}, 
      author={Luke Bailey and Kaiyue Wen and Kefan Dong and Tatsunori Hashimoto and Tengyu Ma},
      year={2026},
      eprint={2604.20209},
      archivePrefix={arXiv},
      primaryClass={cs.LG},
      url={https://arxiv.org/abs/2604.20209}, 
}

@misc{henniger2026tokengamesevaluatinglanguage,
      title={The Token Games: Evaluating Language Model Reasoning with Puzzle Duels}, 
      author={Simon Henniger and Gabriel Poesia},
      year={2026},
      eprint={2602.17831},
      archivePrefix={arXiv},
      primaryClass={cs.AI},
      url={https://arxiv.org/abs/2602.17831}, 
}

@article{wang2020learning,
  title={Learning to prove theorems by learning to generate theorems},
  author={Wang, Mingzhe and Deng, Jia},
  journal={Advances in neural information processing systems},
  volume={33},
  pages={18146--18157},
  year={2020}
}

@article{trinh2024solving,
  title={Solving olympiad geometry without human demonstrations},
  author={Trinh, Trieu H and Wu, Yuhuai and Le, Quoc V and He, He and Luong, Thang},
  journal={Nature},
  volume={625},
  number={7995},
  pages={476--482},
  year={2024},
  publisher={Nature Publishing Group UK London}
}

@article{novikov2025alphaevolve,
  title={Alphaevolve: A coding agent for scientific and algorithmic discovery},
  author={Novikov, Alexander and V{\~u}, Ng{\^a}n and Eisenberger, Marvin and Dupont, Emilien and Huang, Po-Sen and Wagner, Adam Zsolt and Shirobokov, Sergey and Kozlovskii, Borislav and Ruiz, Francisco JR and Mehrabian, Abbas and others},
  journal={arXiv preprint arXiv:2506.13131},
  year={2025}
}

@misc{zheng2026problemproblemscalablemathematical,
      title={The Problem Is the Problem: Towards Scalable Mathematical Discovery}, 
      author={Zeyu Zheng and Shengtong Zhang and Jeremy Avigad and Prasad Tetali and Sean Welleck},
      year={2026},
      eprint={2608.16977},
      archivePrefix={arXiv},
      primaryClass={cs.AI},
      url={https://arxiv.org/abs/2608.16977}, 
}

@misc{polu2020generativelanguagemodelingautomated,
      title={Generative Language Modeling for Automated Theorem Proving}, 
      author={Stanislas Polu and Ilya Sutskever},
      year={2020},
      eprint={2009.03393},
      archivePrefix={arXiv},
      primaryClass={cs.LG},
      url={https://arxiv.org/abs/2009.03393}, 
}

@misc{lample2022hypertreeproofsearchneural,
      title={HyperTree Proof Search for Neural Theorem Proving}, 
      author={Guillaume Lample and Marie-Anne Lachaux and Thibaut Lavril and Xavier Martinet and Amaury Hayat and Gabriel Ebner and Aurélien Rodriguez and Timothée Lacroix},
      year={2022},
      eprint={2205.11491},
      archivePrefix={arXiv},
      primaryClass={cs.CL},
      url={https://arxiv.org/abs/2205.11491}, 
}

@techreport{anthropic2026claudeopus48,
  title={Claude Opus 4.8 System Card},
  author={Anthropic},
  year={2026},
  institution={Anthropic},
  url={https://www-cdn.anthropic.com/0b4915911bb0d19eca5b5ee635c80fef830a37ea.pdf}
}

@misc{openai2026gpt56systemcard,
  title     = {GPT-5.6 System Card},
  author    = {OpenAI},
  year      = {2026},
  url       = {https://deploymentsafety.openai.com/gpt-5-6},
}