HEXAGONbeta

BLLM: Beyond the LLM with Deep Human-Mind-AI

A mix of human-written and AI-generated textHuman understanding: some partscs.AI — Artificial Intelligencemath.PR — Probabilitycs.IT — Information Theory

Contributed by Deep Bhattacharjee ↗, Ushashi Bhattacharya ↗

Version 1 / Oct 20, 2026 / CC BY 4.0

Abstract

A system that improves itself keeps every change that passes a check, so a check that makes errors lets mistakes pile up. We compute the least checking that keeps such a system sound. It is an entropy of the costs of the changes, and an endless chain of improvements stays sound at finite cost exactly when that entropy is finite. A stack of checked layers costs more than its layers would cost alone. We also compute how many guesses a proposer needs before a right one appears: human authors come close to this least number, and language models need 1.5 to 4.3 times as many. Anaxia, an engine built on these laws, rebuilt the published 2016 counterexample to Steinberg's conjecture from the rules of a colouring problem alone. The engine is a work in progress, and its rules and search are being revised and extended for the open problems it has not yet settled.

Provenance statement

The proofs, the text, the figures, the Lean 4 formalization, the engine Anaxia and its benchmarks, and the C, C++, Julia, Python and shell programs were carried out by Deep Bhattacharjee with the help of AI assistance (Claude, Anthropic) in the Claude Code environment. In a model with independent runs, perfect completeness and schedules fixed in advance, the paper proves that the least cost of a sound schedule of randomized checks is an entropy (Theorem A), that Kraft vectors and Huffman codes give the exact optimum (Theorem B), that Renyi entropies govern checks of polynomial order (Theorem C), that a singular chain can be sound exactly when the entropy series of its check costs converges (Theorem D), that a branching takeoff needs linearly growing check strength (Theorem E), the chain law (Theorem F), the online law (Theorem G), the laws of subagents and cascades (Theorems H and XI.1), the gap law (Theorem I: a proposer needs at least exp(H_{1/2}(pi)) proposals), and the tower law (Theorem XIV.1: n verified layers sharing one budget theta cost at least n log(n/theta), and past a finite depth every tower costs more than any fixed amount). The experiments measure the engine Anaxia, a typed crossing network with shared memory, on five open problems: typed crossing reproduces a lattice mass gap for SU(2) on beta_W < 1/3 (Theorem XVII.4, proved in the paper, not refereed, a strong-coupling lattice result and not the Clay problem), memory halves the checks, boosters add nothing, and none of the five problems is solved. Construction mode rebuilds from the rules of Steinberg's problem the gadgets of the 2016 counterexample of Cohen-Addad, Hebdige, Kral', Li and Salgado and the counterexample itself; these are rediscoveries of a published construction. At equal budgets of exact checks a second layer of builders, whose curriculum turns an easier gadget into a lemma, reaches the second gadget where the builder alone never does, and a third layer adds nothing; nothing is found on Erdos's question for cycles of length 4 to 6. Twelve rounds on the Hodge conjecture alone leave every gap where it was. Lemma XVII.1 and Theorem XVII.2 give the exact values of f(n) for Erdos problem 1183 for n <= 20, with f(20) = 12; the lower bound at n = 20 is Theorem 7.6 of the fifth version of Bhattacharjee, Mandal and Bhattacharya (doi:10.5281/zenodo.23374973), whose proof ends in a finite check. Every finite inequality is proved in Lean 4 with Mathlib in sixty-five theorems that depend only on propext, Classical.choice and Quot.sound, with no sorry, native_decide or added axiom. The probabilistic limit theorems are proved or cited in the text and are not formalized. Independent Python, C and C++ programs run 55,271 checks with no failure; no statement rests on them. Both authors approved the final version. Tools used: Anthropic - Claude (Claude Code); Lean community - Lean 4 (v4.33.0) with Mathlib; C; C++; Julia; Python; shell. arXiv identifier: none (not posted on arXiv). Formalization: https://github.com/creelie/eBLLM/tree/main/paper/bllm/lean, package eBLLM and engine Anaxia, release v3.0.0, https://doi.org/10.5281/zenodo.23464390 (all versions: https://doi.org/10.5281/zenodo.23286641)
AI provenance filesAI_PROVENANCE_BLLM.md · 6 KB

Tools used

Anthropic
Claude CodeVersion Fable 5.1 Medium

References

  1. T. Achim, A. Best, A. Bietti, K. Der et al., Aristotle: IMO-level automated theorem proving , preprint (2025). arXiv:2510.01346 (https://arxiv.org/abs/2510.01346).arXiv
  2. G. Ancona, M. Cavicchi, R. Laterveer and G. Saccà, Relative and absolute Lefschetz standard conjectures for some Lagrangian fibrations , J. Lond. Math. Soc. (2) 111 (2025), e70133. doi:10.1112/jlms.70133 (https://doi.org/10.1112/jlms.70133).DOI
  3. S. Arora, C. Lund, R. Motwani, M. Sudan and M. Szegedy, Proof verification and the hardness of approximation problems , J. ACM 45 (1998), no. 3, 501--555. doi:10.1145/278298.278306 (https://doi.org/10.1145/278298.278306).DOI
  4. K. B. Athreya and P. E. Ney, Branching Processes , Grundlehren der mathematischen Wissenschaften 196, Springer, Berlin, 1972. doi:10.1007/978-3-642-65371-1 (https://doi.org/10.1007/978-3-642-65371-1).DOI
  5. Anthropic, Formalizing Fermat's Last Theorem , research report (4 September 2026). https://www.anthropic.com/research/formalizing-fermats-last-theorem.link
  6. A. Anbar Jafari, C. Ozcinar and G. Anbarjafari, A mathematical framework for AI singularity: conditions, bounds, and control of recursive improvement , preprint (2025). arXiv:2511.10668 (https://arxiv.org/abs/2511.10668).arXiv
  7. D. Arapura, Motivation for Hodge cycles , Adv. Math. 207 (2006), 762--781. doi:10.1016/j.aim.2006.01.005 (https://doi.org/10.1016/j.aim.2006.01.005).DOI
  8. OpenAI, Finite-time blowup for Navier--Stokes: OpenAI's Lean proof, built and checked , Zenodo archive, version 1.0.0 (2026). doi:10.5281/zenodo.23286556 (https://doi.org/10.5281/zenodo.23286556).DOI
  9. Z. Zhang, A. Delaval, L. Chen, J. Chen, J. Xu, Y. Liao, J. Jiang, C. Liu and B. Dong, The Poincaré conjecture in Lean 4: the frenzymath formalization, built and checked , Zenodo archive, version 1.0.0 (2026). doi:10.5281/zenodo.23288534 (https://doi.org/10.5281/zenodo.23288534).DOI
  10. S. Hariharan, C. Birkbeck, S. Lee, H. K. G. Ma, B. Mehta, A. Poiroux, M. Viazovska and Math, Inc., Sphere packing in dimensions 8, 24 and 3: an independent check of the formal proofs , Zenodo archive, version 1.0.0 (2026). doi:10.5281/zenodo.23289869 (https://doi.org/10.5281/zenodo.23289869).DOI
Show all 191 referencesShow fewer references
  1. S. Arora and S. Safra, Probabilistic checking of proofs: a new characterization of NP , J. ACM 45 (1998), no. 1, 70--122. doi:10.1145/273865.273901 (https://doi.org/10.1145/273865.273901).DOI
  2. S. Aaronson and A. Wigderson, Algebrization: a new barrier in complexity theory , ACM Trans. Comput. Theory 1 (2009), 2:1--2:54. doi:10.1145/1490270.1490272 (https://doi.org/10.1145/1490270.1490272).DOI
  3. L. Babai, Trading group theory for randomness , in Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing (STOC '85), ACM, New York, 1985, 421--429. doi:10.1145/22145.22192 (https://doi.org/10.1145/22145.22192).DOI
  4. T. Bałaban, Renormalization group approach to lattice gauge field theories. I. Generation of effective actions in a small field approximation and a coupling constant renormalization in four dimensions , Comm. Math. Phys. 109 (1987), 249--301. doi:10.1007/BF01215223 (https://doi.org/10.1007/BF01215223).DOI
  5. G. G. Batrouni, Plaquette formulation and the Bianchi identity for lattice gauge theories , Nuclear Phys. B 208 (1982), 467--483. doi:10.1016/0550-3213(82)90231-0 (https://doi.org/10.1016/0550-3213(82)90231-0).DOI
  6. R. Bauerschmidt and T. Bodineau, Log-Sobolev inequality for the continuum sine-Gordon model , Comm. Pure Appl. Math. 74 (2021), 2064--2113. doi:10.1002/cpa.21926 (https://doi.org/10.1002/cpa.21926).DOI
  7. D. Bhattacharjee and U. Bhattacharya, Dense algebraic loci of Hodge classes , Hexagon preprint (2026), hexagon:2610.00315v1, hexagonmath.org/2610.00315v1 (https://hexagonmath.org/2610.00315v1); source and Lean 4 archive, version 2.0.0, doi:10.5281/zenodo.23461752 (https://doi.org/10.5281/zenodo.23461752).hexagonDOI
  8. D. Bhattacharjee and U. Bhattacharya, Lattice Yang--Mills theory: spacing-uniform obstructions, the mass gap up to the Dobrushin ceiling, and Lean certificate , Zenodo, version 2.0.0 (2026). doi:10.5281/zenodo.23449466 (https://doi.org/10.5281/zenodo.23449466).DOI
  9. M.-F. Balcan, A. Blum, K. Fragkia, Z. Li and D. Sharma, Verify to amplify: improving reasoning via learned chain-of-thought verification , preprint (2026). arXiv:2603.03538 (https://arxiv.org/abs/2603.03538).arXiv
  10. A. Bastounis, F. Circelli and A. C. Hansen, Navier--Stokes lost in translation: why Lean verification of AI autoformalisation does not guarantee correct natural language proofs , preprint (2026). arXiv:2610.08144 (https://arxiv.org/abs/2610.08144).arXiv
  11. O. V. Borodin, A. N. Glebov, A. Raspaud and M. R. Salavatipour, Planar graphs without cycles of length from 44 to 77 are 33-colorable , J. Combin. Theory Ser. B 93 (2005), 303--311. doi:10.1016/j.jctb.2004.11.001 (https://doi.org/10.1016/j.jctb.2004.11.001).DOI
  12. T. Baker, J. Gill and R. Solovay, Relativizations of the P=?NP\mathcal{P}=?\mathcal{NP} question , SIAM J. Comput. 4 (1975), 431--442. doi:10.1137/0204037 (https://doi.org/10.1137/0204037).DOI
  13. D. Bhattacharjee, Synthetic neuromorphic superintelligence for verifier-gated conjecture closure: sand-tile automata, K-dot circuits, and phenomenological proof learning , PhilArchive (2026). philarchive.org/rec/BHASNS-2 (https://philarchive.org/rec/BHASNS-2).link
  14. D. Bhattacharjee, Anaxia, the BLLM engine , Python package eBLLM with the command anaxia , Lean 4 library and container image ghcr.io/creelie/bllm-engine , Zenodo, release (2026), ; all versions doi:10.5281/zenodo.23286641 (https://doi.org/10.5281/zenodo.23286641). github.com/creelie/eBLLM (https://github.com/creelie/eBLLM).DOI
  15. B. Brown, J. Juravsky, R. Ehrlich, R. Clark, Q. V. Le, C. Ré and A. Mirhoseini, Large language monkeys: scaling inference compute with repeated sampling , preprint (2024). arXiv:2407.21787 (https://arxiv.org/abs/2407.21787).arXiv
  16. Y. Bai, S. Kadavath, S. Kundu, A. Askell, J. Kernion, A. Jones et al., Constitutional AI: harmlessness from AI feedback , preprint (2022). arXiv:2212.08073 (https://arxiv.org/abs/2212.08073).arXiv
  17. E. Botta, Y. Li, A. Mehta, J. T. Ash, C. Zhang and A. Risteski, On the query complexity of verifier-assisted language generation , preprint (2025). arXiv:2502.12123 (https://arxiv.org/abs/2502.12123).arXiv
  18. T. F. Bloom, Erdős problem #1183 , erdosproblems.com/1183 (https://www.erdosproblems.com/1183), accessed 18 October 2026.link
  19. D. Bhattacharjee, P. Mandal and U. Bhattacharya, Resolving Erdős--Ulam monochromatic union-closed family conjectures , preprint (2026), arXiv:2610.02833 (https://arxiv.org/abs/2610.02833); Lean 4 archive, version 5, doi:10.5281/zenodo.23374973 (https://doi.org/10.5281/zenodo.23374973).arXivDOI
  20. D. Bhattacharjee, P. Mandal and U. Bhattacharya, Algebraic loci of Weil classes on abelian varieties , with verification code, Zenodo, version 5.0.1 (2026). doi:10.5281/zenodo.23225483 (https://doi.org/10.5281/zenodo.23225483).DOI
  21. T. B. Brown, B. Mann, N. Ryder, M. Subbiah, J. Kaplan, P. Dhariwal et al., Language models are few-shot learners , Advances in Neural Information Processing Systems 33 (2020), 1877--1901. arXiv:2005.14165 (https://arxiv.org/abs/2005.14165).arXiv
  22. É. Borel, Les probabilités dénombrables et leurs applications arithmétiques , Rend. Circ. Mat. Palermo 27 (1909), 247--271. doi:10.1007/BF03019651 (https://doi.org/10.1007/BF03019651).DOI
  23. N. Bostrom, The superintelligent will: motivation and instrumental rationality in advanced artificial agents , Minds and Machines 22 (2012), 71--85. doi:10.1007/s11023-012-9281-3 (https://doi.org/10.1007/s11023-012-9281-3).DOI
  24. N. Bostrom, Superintelligence: Paths, Dangers, Strategies , Oxford University Press, Oxford, 2014.
  25. N. Bostrom, How long before superintelligence? , Int. J. Futures Studies 2 (1998); reprinted in Linguistic and Philosophical Investigations 5 (2006), no. 1, 11--30.
  26. M. Bhargava and A. Shankar, Binary quartic forms having bounded invariants, and the boundedness of the average rank of elliptic curves , Ann. of Math. (2) 181 (2015), 191--242. doi:10.4007/annals.2015.181.1.3 (https://doi.org/10.4007/annals.2015.181.1.3).DOI
  27. M. Bhargava and A. Shankar, Ternary cubic forms having bounded invariants, and the existence of a positive proportion of elliptic curves having rank 00 , Ann. of Math. (2) 181 (2015), 587--621. doi:10.4007/annals.2015.181.2.4 (https://doi.org/10.4007/annals.2015.181.2.4).DOI
  28. N. Buskin, Every rational Hodge isometry between two K3 surfaces is algebraic , J. Reine Angew. Math. 755 (2019), 127--150. doi:10.1515/crelle-2017-0027 (https://doi.org/10.1515/crelle-2017-0027).DOI
  29. L. L. Campbell, A coding theorem and Rényi's entropy , Information and Control 8 (1965), no. 4, 423--429. doi:10.1016/S0019-9958(65)90332-3 (https://doi.org/10.1016/S0019-9958(65)90332-3).DOI
  30. H. Cohn and N. Elkies, New upper bounds on sphere packings I , Ann. of Math. 157 (2003), 689--714. doi:10.4007/annals.2003.157.689 (https://doi.org/10.4007/annals.2003.157.689).DOI
  31. L. Chen, J. Gu, L. Huang, W. Huang et al., Seed-Prover: deep and broad reasoning for automated theorem proving , preprint (2025). arXiv:2507.23726 (https://arxiv.org/abs/2507.23726).arXiv
  32. H. Chernoff, A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations , Ann. Math. Statist. 23 (1952), no. 4, 493--507. doi:10.1214/aoms/1177729330 (https://doi.org/10.1214/aoms/1177729330).DOI
  33. V. Cohen-Addad, M. Hebdige, D. Král', Z. Li and E. Salgado, Steinberg's conjecture is false , J. Combin. Theory Ser. B 122 (2017), 452--456. doi:10.1016/j.jctb.2016.07.006 (https://doi.org/10.1016/j.jctb.2016.07.006).DOI
  34. P. Chojecki, Monochromatic union-closed and lattice subfamilies of the Boolean lattice , preprint (18 March 2026). https://www.ulam.ai/research/erdos1183.pdf.link
  35. S. J. Cook, T. A. Jarrell, C. A. Brittin, Y. Wang et al., Whole-animal connectomes of both Caenorhabditis elegans sexes , Nature 571 (2019), 63--71. doi:10.1038/s41586-019-1352-7 (https://doi.org/10.1038/s41586-019-1352-7).DOI
  36. K. Cobbe, V. Kosaraju, M. Bavarian, M. Chen, H. Jun, L. Kaiser et al., Training verifiers to solve math word problems , preprint (2021). arXiv:2110.14168 (https://arxiv.org/abs/2110.14168).arXiv
  37. H. Cohn, A. Kumar, S. D. Miller, D. Radchenko and M. Viazovska, The sphere packing problem in dimension 24 , Ann. of Math. (2) 185 (2017), no. 3, 1017--1033. doi:10.4007/annals.2017.185.3.8 (https://doi.org/10.4007/annals.2017.185.3.8).DOI
  38. Clay Mathematics Institute, The Millennium Prize Problems , https://www.claymath.org/millennium-problems/, accessed 18 October 2026.link
  39. F. Charles and E. Markman, The standard conjectures for holomorphic symplectic varieties deformation equivalent to Hilbert schemes of K3 surfaces , Compos. Math. 149 (2013), 481--494. doi:10.1112/S0010437X12000607 (https://doi.org/10.1112/S0010437X12000607).DOI
  40. S. Chen, K. Marwaha, X. Lu, H. Yuen and T. Peng, Prove2Me: an open collaborative platform for scaling math formalization , preprint (2026). arXiv:2608.28433 (https://arxiv.org/abs/2608.28433).arXiv
  41. M. Creutz, Gauge fixing, the transfer matrix, and confinement on a lattice , Phys. Rev. D 15 (1977), 1128--1136. doi:10.1103/PhysRevD.15.1128 (https://doi.org/10.1103/PhysRevD.15.1128).DOI
  42. M. Creutz, Monte Carlo study of quantized SU(2) gauge theory , Phys. Rev. D 21 (1980), 2308--2315. doi:10.1103/PhysRevD.21.2308 (https://doi.org/10.1103/PhysRevD.21.2308).DOI
  43. T. M. Cover and J. A. Thomas, Elements of Information Theory , 2nd ed., Wiley, Hoboken, 2006. doi:10.1002/047174882X (https://doi.org/10.1002/047174882X).DOI
  44. Yu. Chervonyi, T. H. Trinh, M. Olšák, X. Yang et al., Gold-medalist performance in solving olympiad geometry with AlphaGeometry2 , preprint (2025). arXiv:2502.03544 (https://arxiv.org/abs/2502.03544).arXiv
  45. Z. Chen, Y. Zhao and A. Cohan, Measuring the gap between human and LLM research ideas , preprint (2026). arXiv:2607.01233 (https://arxiv.org/abs/2607.01233).arXiv
  46. N. G. de Bruijn, The mathematical language AUTOMATH, its usage, and some of its extensions , in Symposium on Automatic Demonstration, Lecture Notes in Math. 125, Springer, Berlin, 1970, 29--61. doi:10.1007/BFb0060623 (https://doi.org/10.1007/BFb0060623).DOI
  47. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem , Current Developments in Mathematics 1995 (1995), 1--154. doi:10.4310/CDM.1995.v1995.n1.a1 (https://doi.org/10.4310/CDM.1995.v1995.n1.a1).DOI
  48. N. Dziri, X. Lu, M. Sclar, X. L. Li, L. Jiang, B. Y. Lin et al., Faith and fate: limits of transformers on compositionality , Advances in Neural Information Processing Systems 36 (2023). arXiv:2305.18654 (https://arxiv.org/abs/2305.18654).arXiv
  49. R. J. Douglas and K. A. C. Martin, Neuronal circuits of the neocortex , Annu. Rev. Neurosci. 27 (2004), 419--451. doi:10.1146/annurev.neuro.27.070203.144152 (https://doi.org/10.1146/annurev.neuro.27.070203.144152).DOI
  50. S. Dorkenwald, A. Matsliah, A. R. Sterling, P. Schlegel, S.-C. Yu, C. E. McKellar et al., Neuronal wiring diagram of an adult brain , Nature 634 (2024), 124--138. doi:10.1038/s41586-024-07558-y (https://doi.org/10.1038/s41586-024-07558-y).DOI
  51. R. L. Dobrushin, The description of a random field by means of conditional probabilities and conditions of its regularity , Theory Probab. Appl. 13 (1968), 197--224. doi:10.1137/1113026 (https://doi.org/10.1137/1113026).DOI
  52. M. Davies, N. Srinivasa, T.-H. Lin, G. Chinya et al., Loihi: a neuromorphic manycore processor with on-chip learning , IEEE Micro 38 (2018), no. 1, 82--99. doi:10.1109/MM.2018.112130359 (https://doi.org/10.1109/MM.2018.112130359).DOI
  53. R. Durrett, Probability: Theory and Examples , 5th ed., Cambridge University Press, Cambridge, 2019. doi:10.1017/9781108591034 (https://doi.org/10.1017/9781108591034).DOI
  54. A. Davies, P. Veličković, L. Buesing, S. Blackwell, D. Zheng, N. Tomašev et al., Advancing mathematics by guiding human intuition with AI , Nature 600 (2021), no. 7887, 70--74. doi:10.1038/s41586-021-04086-x (https://doi.org/10.1038/s41586-021-04086-x).DOI
  55. M. Dwass, The total progeny in a branching process and a related random walk , J. Appl. Probab. 6 (1969), no. 3, 682--686. doi:10.2307/3212112 (https://doi.org/10.2307/3212112).DOI
  56. N. Eckstein, A. S. Bates, A. Champion, M. Du et al., Neurotransmitter classification from electron microscopy images at synaptic sites in Drosophila melanogaster , Cell 187 (2024), 2574--2594. doi:10.1016/j.cell.2024.03.016 (https://doi.org/10.1016/j.cell.2024.03.016).DOI
  57. P. Elias, Universal codeword sets and representations of the integers , IEEE Trans. Inform. Theory 21 (1975), no. 2, 194--203. doi:10.1109/TIT.1975.1055349 (https://doi.org/10.1109/TIT.1975.1055349).DOI
  58. A. Fawzi, M. Balog, A. Huang, T. Hubert, B. Romera-Paredes, M. Barekatain et al., Discovering faster matrix multiplication algorithms with reinforcement learning , Nature 610 (2022), no. 7930, 47--53. doi:10.1038/s41586-022-05172-4 (https://doi.org/10.1038/s41586-022-05172-4).DOI
  59. The Formal Conjectures Authors, Formal Conjectures , Lean 4 statements of open and solved conjectures, Google DeepMind (2025). github.com/google-deepmind/formal-conjectures (https://github.com/google-deepmind/formal-conjectures).link
  60. N. Frémaux and W. Gerstner, Neuromodulated spike-timing-dependent plasticity, and theory of three-factor learning rules , Front. Neural Circuits 9 (2016), 85. doi:10.3389/fncir.2015.00085 (https://doi.org/10.3389/fncir.2015.00085).DOI
  61. S. Floccari, On the motive of O'Grady's six dimensional hyper-Kähler varieties , Épijournal Géom. Algébrique 7 (2023). doi:10.46298/epiga.2022.9758 (https://doi.org/10.46298/epiga.2022.9758).DOI
  62. J. Foster, The Lefschetz standard conjectures for IHSMs of generalized Kummer deformation type in certain degrees , preprint (2023). arXiv:2303.14327 (https://arxiv.org/abs/2303.14327).arXiv
  63. J. Foster, The Lefschetz standard conjectures for 4d4d-dimensional Kummer-type hyper-Kähler varieties , preprint (2025). arXiv:2512.04114 (https://arxiv.org/abs/2512.04114).arXiv
  64. R. G. Gallager, Variations on a theme by Huffman , IEEE Trans. Inform. Theory 24 (1978), no. 6, 668--674. doi:10.1109/TIT.1978.1055959 (https://doi.org/10.1109/TIT.1978.1055959).DOI
  65. B. Georgiev, J. Gómez-Serrano, T. Tao and A. Z. Wagner, Mathematical exploration and discovery at scale , preprint (2025). arXiv:2511.02864 (https://arxiv.org/abs/2511.02864).arXiv
  66. W. Gerstner, W. M. Kistler, R. Naud and L. Paninski, Neuronal Dynamics: From Single Neurons to Networks and Models of Cognition , Cambridge University Press, Cambridge, 2014. doi:10.1017/CBO9781107447615 (https://doi.org/10.1017/CBO9781107447615).DOI
  67. S. Goldwasser, S. Micali and C. Rackoff, The knowledge complexity of interactive proof systems , SIAM J. Comput. 18 (1989), no. 1, 186--208. doi:10.1137/0218012 (https://doi.org/10.1137/0218012).DOI
  68. M. J. Gordon, A. J. Milner and C. P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation , Lecture Notes in Comput. Sci. 78, Springer, Berlin, 1979. doi:10.1007/3-540-09724-4 (https://doi.org/10.1007/3-540-09724-4).DOI
  69. K. Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I , Monatsh. Math. Phys. 38 (1931), 173--198. doi:10.1007/BF01700692 (https://doi.org/10.1007/BF01700692).DOI
  70. I. J. Good, Speculations concerning the first ultraintelligent machine , Advances in Computers 6 (1966), 31--88. doi:10.1016/S0065-2458(08)60418-0 (https://doi.org/10.1016/S0065-2458(08)60418-0).DOI
  71. D. Guo, The deterministic horizon: impossibility results as design specifications for trustworthy AI systems , preprint (2026). arXiv:2605.23024 (https://arxiv.org/abs/2605.23024).arXiv
  72. B. H. Gross and D. B. Zagier, Heegner points and derivatives of LL-series , Invent. Math. 84 (1986), 225--320. doi:10.1007/BF01388809 (https://doi.org/10.1007/BF01388809).DOI
  73. A. Hatcher, Algebraic Topology , Cambridge University Press, Cambridge, 2002.
  74. S. Hariharan, C. Birkbeck, S. Lee, H. K. G. Ma, B. Mehta, A. Poiroux and M. Viazovska, Progress in formalizing sphere packing in dimension 8 , preprint (2026). arXiv:2604.23468 (https://arxiv.org/abs/2604.23468).arXiv
  75. J. Hoffmann, S. Borgeaud, A. Mensch, E. Buchatskaya, T. Cai, E. Rutherford et al., Training compute-optimal large language models , preprint (2022). arXiv:2203.15556 (https://arxiv.org/abs/2203.15556).arXiv
  76. D. O. Hebb, The Organization of Behavior: A Neuropsychological Theory , Wiley, New York, 1949.
  77. J. Huang, S. S. Gu, L. Hou, Y. Wu, X. Wang, H. Yu and J. Han, Large language models can self-improve , preprint (2022). arXiv:2210.11610 (https://arxiv.org/abs/2210.11610).arXiv
  78. X.-D. Hou, K. H. Leung and Q. Xiang, A generalization of an addition theorem of Kneser , J. Number Theory 97 (2002), no. 1, 1--9. doi:10.1006/jnth.2002.2793 (https://doi.org/10.1006/jnth.2002.2793).DOI
  79. T. Hubert, R. Mehta, L. Sartran, M. Z. Horváth, G. Žužić, E. Wieser et al., Olympiad-level formal mathematical reasoning with reinforcement learning , Nature 651 (2026), no. 8106, 607--613; published online 2025. doi:10.1038/s41586-025-09833-y (https://doi.org/10.1038/s41586-025-09833-y).DOI
  80. W. Hoeffding, Probability inequalities for sums of bounded random variables , J. Amer. Statist. Assoc. 58 (1963), no. 301, 13--30. doi:10.1080/01621459.1963.10500830 (https://doi.org/10.1080/01621459.1963.10500830).DOI
  81. H. A. Helfgott and M. Radziwiłł, Expansion, divisibility and parity , preprint (2021). arXiv:2103.06853 (https://arxiv.org/abs/2103.06853).arXiv
  82. D. A. Huffman, A method for the construction of minimum-redundancy codes , Proc. IRE 40 (1952), no. 9, 1098--1101. doi:10.1109/JRPROC.1952.273898 (https://doi.org/10.1109/JRPROC.1952.273898).DOI
  83. M. Hutter, Universal Artificial Intelligence: Sequential Decisions Based on Algorithmic Probability , Springer, Berlin, 2005. doi:10.1007/b138233 (https://doi.org/10.1007/b138233).DOI
  84. J. L. W. V. Jensen, Sur les fonctions convexes et les inégalités entre les valeurs moyennes , Acta Math. 30 (1906), 175--193. doi:10.1007/BF02418571 (https://doi.org/10.1007/BF02418571).DOI
  85. H. Jaeger and H. Haas, Harnessing nonlinearity: predicting chaotic systems and saving energy in wireless communication , Science 304 (2004), 78--80. doi:10.1126/science.1091277 (https://doi.org/10.1126/science.1091277).DOI
  86. Z. Jia, A. Rakhlin and T. Xie, Do we need to verify step by step? Rethinking process supervision from a theoretical perspective , preprint (2025). arXiv:2502.10581 (https://arxiv.org/abs/2502.10581).arXiv
  87. K. Jamieson and A. Talwalkar, Non-stochastic best arm identification and hyperparameter optimization , in Proceedings of the 19th International Conference on Artificial Intelligence and Statistics (2016). arXiv:1502.07943 (https://arxiv.org/abs/1502.07943).arXiv
  88. S. L. Kleiman, The standard conjectures , in Motives (Seattle, 1991), Proc. Sympos. Pure Math. 55, Part 1, Amer. Math. Soc., Providence, 1994, 3--20. doi:10.1090/pspum/055.1/1265519 (https://doi.org/10.1090/pspum/055.1/1265519).DOI
  89. J. Kaplan, S. McCandlish, T. Henighan, T. B. Brown, B. Chess, R. Child, S. Gray, A. Radford, J. Wu and D. Amodei, Scaling laws for neural language models , preprint (2020). arXiv:2001.08361 (https://arxiv.org/abs/2001.08361).arXiv
  90. V. A. Kolyvagin, Finiteness of E(Q)E(\mathbf{Q}) and Sha(E,Q)(E,\mathbf{Q}) for a subclass of Weil curves , Math. USSR-Izv. 32 (1989), 523--541. doi:10.1070/IM1989v032n03ABEH000779 (https://doi.org/10.1070/IM1989v032n03ABEH000779).DOI
  91. L. G. Kraft, A device for quantizing, grouping, and coding amplitude-modulated pulses , M.S. thesis, Massachusetts Institute of Technology, 1949. hdl:1721.1/12390 (https://hdl.handle.net/1721.1/12390).link
  92. H. Kesten and B. P. Stigum, A limit theorem for multidimensional Galton--Watson processes , Ann. Math. Statist. 37 (1966), no. 5, 1211--1223. doi:10.1214/aoms/1177699266 (https://doi.org/10.1214/aoms/1177699266).DOI
  93. C. Liu, Y. Chen, T. Liu, J. Cheng, B. Han and K. Zhang, On the thinking-language modeling gap in large language models , preprint (2025). arXiv:2505.12896 (https://arxiv.org/abs/2505.12896).arXiv
  94. T. Leelawat and L. D. Griffin, Watson & Holmes: a naturalistic benchmark for comparing human and LLM reasoning , preprint (2026). arXiv:2602.19914 (https://arxiv.org/abs/2602.19914).arXiv
  95. D. I. Lieberman, Numerical and homological equivalence of algebraic cycles on Hodge manifolds , Amer. J. Math. 90 (1968), 366--374. doi:10.2307/2373533 (https://doi.org/10.2307/2373533).DOI
  96. H. Lightman, V. Kosaraju, Y. Burda, H. Edwards, B. Baker, T. Lee, J. Leike, J. Schulman, I. Sutskever and K. Cobbe, Let's verify step by step , preprint (2023). arXiv:2305.20050 (https://arxiv.org/abs/2305.20050).arXiv
  97. G. Lample, M.-A. Lachaux, T. Lavril, X. Martinet et al., HyperTree proof search for neural theorem proving , Advances in Neural Information Processing Systems 35 (2022). arXiv:2205.11491 (https://arxiv.org/abs/2205.11491).arXiv
  98. M. H. Löb, Solution of a problem of Leon Henkin , J. Symbolic Logic 20 (1955), no. 2, 115--118. doi:10.2307/2266895 (https://doi.org/10.2307/2266895).DOI
  99. Y. Lin, S. Tang, B. Lyu, J. Wu et al., Goedel-Prover: a frontier model for open-source automated theorem proving , preprint (2025). arXiv:2502.07640 (https://arxiv.org/abs/2502.07640).arXiv
  100. J. K. Lappalainen, F. D. Tschopp, S. Prakhya, M. McGill et al., Connectome-constrained networks predict neural activity across the fly visual system , Nature 634 (2024), 1132--1140. doi:10.1038/s41586-024-07939-3 (https://doi.org/10.1038/s41586-024-07939-3).DOI
  101. C.-P. Lu, Verification and self-improvement in agentic AI: foundations and limits , preprint (2026). arXiv:2610.10611 (https://arxiv.org/abs/2610.10611).arXiv
  102. M. Lüscher, Properties and uses of the Wilson flow in lattice QCD , J. High Energy Phys. 2010 (2010), no. 8, 071. doi:10.1007/JHEP08(2010)071 (https://doi.org/10.1007/JHEP08(2010)071).DOI
  103. W. Maass, Networks of spiking neurons: the third generation of neural network models , Neural Networks 10 (1997), 1659--1671. doi:10.1016/S0893-6080(97)00011-7 (https://doi.org/10.1016/S0893-6080(97)00011-7).DOI
  104. E. Markman, Cycles on abelian 2n2n-folds of Weil type from secant sheaves on abelian nn-folds , preprint (2025), arXiv:2502.03415 (https://arxiv.org/abs/2502.03415).arXiv
  105. B. McMillan, Two inequalities implied by unique decipherability , IRE Trans. Inform. Theory 2 (1956), no. 4, 115--116. doi:10.1109/TIT.1956.1056818 (https://doi.org/10.1109/TIT.1956.1056818).DOI
  106. C. Mead, Neuromorphic electronic systems , Proc. IEEE 78 (1990), 1629--1636. doi:10.1109/5.58356 (https://doi.org/10.1109/5.58356).DOI
  107. D. J. Mankowitz, A. Michi, A. Zhernov, M. Gelmi, M. Selvi, C. Paduraru et al., Faster sorting algorithms discovered using deep reinforcement learning , Nature 618 (2023), no. 7964, 257--263. doi:10.1038/s41586-023-06004-9 (https://doi.org/10.1038/s41586-023-06004-9).DOI
  108. K. Matomäki, M. Radziwiłł, T. Tao, J. Teräväinen and T. Ziegler, Higher uniformity of bounded multiplicative functions in short intervals on average , Ann. of Math. (2) 197 (2023), 739--857. doi:10.4007/annals.2023.197.2.3 (https://doi.org/10.4007/annals.2023.197.2.3).DOI
  109. A. Madaan, N. Tandon, P. Gupta, S. Hallinan, L. Gao, S. Wiegreffe et al., Self-refine: iterative refinement with self-feedback , Advances in Neural Information Processing Systems 36 (2023). arXiv:2303.17651 (https://arxiv.org/abs/2303.17651).arXiv
  110. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language , in Automated Deduction -- CADE 28, Lecture Notes in Comput. Sci. 12699, Springer, Cham, 2021, 625--635. doi:10.1007/978-3-030-79876-5_37 (https://doi.org/10.1007/978-3-030-79876-5_37).DOI
  111. B. J. J. Moonen and Yu. G. Zarhin, Weil classes on abelian varieties , J. Reine Angew. Math. 496 (1998), 83--92. doi:10.1515/crll.1998.034 (https://doi.org/10.1515/crll.1998.034).DOI
  112. A. Novikov, N. Vũ, M. Eisenberger, E. Dupont et al., AlphaEvolve: a coding agent for scientific and algorithmic discovery , preprint (2025). arXiv:2506.13131 (https://arxiv.org/abs/2506.13131).arXiv
  113. OpenAI, Finite time blowup for Navier--Stokes , preprint (2026), with the Lean 4 formalization openai/NavierStokesAndEuler . cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf (https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf).link
  114. OpenAI, Mathematical manuscripts and proof artifacts , repository openai/math (2026), 722 manuscripts in 372 families; mirror github.com/creelie/math01-openAI (https://github.com/creelie/math01-openAI).link
  115. OpenAI, Ordinary two-point correlations of multiplicative functions , preprint (24 September 2026), with a Lean 4 formalization, in openai/math ; mirror github.com/creelie/math01-openAI (https://github.com/creelie/math01-openAI).link
  116. The Omega Institute, trureturing: a scientific method for AI to discover truth and find its next question , repository (2026), with 782782 problem dossiers and their Lean 4 resolutions; github.com/the-omega-institute/trureturing (https://github.com/the-omega-institute/trureturing); copy github.com/creelie/trureturing-OpenRefute (https://github.com/creelie/trureturing-OpenRefute).link
  117. T. Ord, The dynamics of intelligence explosions , preprint (2026). arXiv:2608.14426 (https://arxiv.org/abs/2608.14426).arXiv
  118. The Omega Institute, trureturing , Lean 4 theorem odd_lower_bound in D5/S3/Combinatorics/ErdosUlam/SublatticeChainBound.lean , repository the-omega-institute/trureturing (2026), commit fa35d5b ; mirror github.com/creelie/trureturing-OpenRefute (https://github.com/creelie/trureturing-OpenRefute).link
  119. K. Osterwalder and E. Seiler, Gauge field theories on a lattice , Ann. Physics 110 (1978), 440--471. doi:10.1016/0003-4916(78)90039-8 (https://doi.org/10.1016/0003-4916(78)90039-8).DOI
  120. W. F. Osgood, Beweis der Existenz einer Lösung der Differentialgleichung dy/dx=f(x,y)dy/dx=f(x,y) ohne Hinzunahme der Cauchy--Lipschitz'schen Bedingung , Monatsh. Math. Phys. 9 (1898), 331--345. doi:10.1007/BF01707876 (https://doi.org/10.1007/BF01707876).DOI
  121. R. Otter, The multiplicative process , Ann. Math. Statist. 20 (1949), no. 2, 206--224. doi:10.1214/aoms/1177730031 (https://doi.org/10.1214/aoms/1177730031).DOI
  122. G. Perelman, The entropy formula for the Ricci flow and its geometric applications , preprint (2002). arXiv:math/0211159 (https://arxiv.org/abs/math/0211159).arXiv
  123. G. Perelman, Ricci flow with surgery on three-manifolds , preprint (2003). arXiv:math/0303109 (https://arxiv.org/abs/math/0303109).arXiv
  124. G. Perelman, Finite extinction time for the solutions to the Ricci flow on certain three-manifolds , preprint (2003). arXiv:math/0307245 (https://arxiv.org/abs/math/0307245).arXiv
  125. C. Pilatte, Improved bounds for the two-point logarithmic Chowla conjecture , preprint (2023). arXiv:2310.19357 (https://arxiv.org/abs/2310.19357).arXiv
  126. C. Pilatte, Improved bounds for the Fourier uniformity conjecture , preprint (2026). arXiv:2604.26564 (https://arxiv.org/abs/2604.26564).arXiv
  127. W. H. Press, Strong profiling is not mathematically optimal for discovering rare malfeasors , Proc. Natl. Acad. Sci. USA 106 (2009), 1716--1719. doi:10.1073/pnas.0813202106 (https://doi.org/10.1073/pnas.0813202106).DOI
  128. K. Pratt, N. Robles, A. Zaharescu and D. Zeindler, More than five-twelfths of the zeros of ζ\zeta are on the critical line , Res. Math. Sci. 7 (2020), 2. doi:10.1007/s40687-019-0199-8 (https://doi.org/10.1007/s40687-019-0199-8).DOI
  129. S. Polu and I. Sutskever, Generative language modeling for automated theorem proving , preprint (2020). arXiv:2009.03393 (https://arxiv.org/abs/2009.03393).arXiv
  130. D. Platt and T. Trudgian, The Riemann hypothesis is true up to 3⋅10123\cdot10^{12} , Bull. Lond. Math. Soc. 53 (2021), 792--797. doi:10.1112/blms.12460 (https://doi.org/10.1112/blms.12460).DOI
  131. Qwen Team (A. Yang et al.), Qwen2.5 technical report , preprint (2024). arXiv:2412.15115 (https://arxiv.org/abs/2412.15115).arXiv
  132. B. Romera-Paredes, M. Barekatain, A. Novikov, M. Balog, M. P. Kumar, E. Dupont et al., Mathematical discoveries from program search with large language models , Nature 625 (2024), no. 7995, 468--475. doi:10.1038/s41586-023-06924-6 (https://doi.org/10.1038/s41586-023-06924-6).DOI
  133. A. Rényi, On measures of entropy and information , in Proceedings of the Fourth Berkeley Symposium on Mathematical Statistics and Probability, vol. 1, University of California Press, Berkeley, 1961, 547--561.
  134. J. Rissanen, A universal prior for integers and estimation by minimum description length , Ann. Statist. 11 (1983), no. 2, 416--431. doi:10.1214/aos/1176346150 (https://doi.org/10.1214/aos/1176346150).DOI
  135. P. Redgrave, T. J. Prescott and K. Gurney, The basal ganglia: a vertebrate solution to the selection problem? , Neuroscience 89 (1999), 1009--1023. doi:10.1016/S0306-4522(98)00319-4 (https://doi.org/10.1016/S0306-4522(98)00319-4).DOI
  136. A. A. Razborov and S. Rudich, Natural proofs , J. Comput. System Sci. 55 (1997), 24--35. doi:10.1006/jcss.1997.1494 (https://doi.org/10.1006/jcss.1997.1494).DOI
  137. D. Rohatgi, A. Shetty, D. Saless, Y. Li, A. Moitra, A. Risteski and D. J. Foster, Taming imperfect process verifiers: a sampling perspective on backtracking , preprint (2025). arXiv:2510.03149 (https://arxiv.org/abs/2510.03149).arXiv
  138. Z. Z. Ren, Z. Shao, J. Song, H. Xin et al., DeepSeek-Prover-V2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition , preprint (2025). arXiv:2504.21801 (https://arxiv.org/abs/2504.21801).arXiv
  139. J. Schmidhuber, Gödel machines: self-referential universal problem solvers making provably optimal self-improvements , preprint (2003). arXiv:cs/0309048 (https://arxiv.org/abs/cs/0309048).arXiv
  140. J. T. Schwartz, Fast probabilistic algorithms for verification of polynomial identities , J. ACM 27 (1980), no. 4, 701--717. doi:10.1145/322217.322225 (https://doi.org/10.1145/322217.322225).DOI
  141. C. Schoen, Addendum to: Hodge classes on self-products of a variety with an automorphism , Compos. Math. 114 (1998), 321--328. doi:10.1023/A:1000566205021 (https://doi.org/10.1023/A:1000566205021).DOI
  142. A. Scrivens, Empirical validation of the classification-verification dichotomy for AI safety gates , preprint (2026). arXiv:2604.00072 (https://arxiv.org/abs/2604.00072).arXiv
  143. W. Schultz, P. Dayan and P. R. Montague, A neural substrate of prediction and reward , Science 275 (1997), 1593--1599. doi:10.1126/science.275.5306.1593 (https://doi.org/10.1126/science.275.5306.1593).DOI
  144. D. Saxton, E. Grefenstette, F. Hill and P. Kohli, Analysing mathematical reasoning abilities of neural models , International Conference on Learning Representations (2019). arXiv:1904.01557 (https://arxiv.org/abs/1904.01557).arXiv
  145. C. E. Shannon, A mathematical theory of communication , Bell System Tech. J. 27 (1948), no. 3, 379--423. doi:10.1002/j.1538-7305.1948.tb01338.x (https://doi.org/10.1002/j.1538-7305.1948.tb01338.x).DOI
  146. T. Shioda, The Hodge conjecture for Fermat varieties , Math. Ann. 245 (1979), 175--184. doi:10.1007/BF01428804 (https://doi.org/10.1007/BF01428804).DOI
  147. D. Silver, A. Huang, C. J. Maddison, A. Guez, L. Sifre, G. van den Driessche et al., Mastering the game of Go with deep neural networks and tree search , Nature 529 (2016), no. 7587, 484--489. doi:10.1038/nature16961 (https://doi.org/10.1038/nature16961).DOI
  148. D. Silver, T. Hubert, J. Schrittwieser, I. Antonoglou, M. Lai, A. Guez et al., A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play , Science 362 (2018), no. 6419, 1140--1144. doi:10.1126/science.aar6404 (https://doi.org/10.1126/science.aar6404).DOI
  149. A. Shapson-Coe, M. Januszewski, D. R. Berger, A. Pope et al., A petavoxel fragment of human cerebral cortex reconstructed at nanoscale resolution , Science 384 (2024), eadk4858. doi:10.1126/science.adk4858 (https://doi.org/10.1126/science.adk4858).DOI
  150. C. Snell, J. Lee, K. Xu and A. Kumar, Scaling LLM test-time compute optimally can be more effective than scaling model parameters , preprint (2024). arXiv:2408.03314 (https://arxiv.org/abs/2408.03314).arXiv
  151. R. J. Solomonoff, A formal theory of inductive inference. Part I , Information and Control 7 (1964), no. 1, 1--22. doi:10.1016/S0019-9958(64)90223-2 (https://doi.org/10.1016/S0019-9958(64)90223-2).DOI
  152. R. Steinberg, The state of the three color problem , in Quo Vadis, Graph Theory? , Ann. Discrete Math. 55 (1993), 211--248. doi:10.1016/S0167-5060(08)70391-1 (https://doi.org/10.1016/S0167-5060(08)70391-1).DOI
  153. N. Seiberg and E. Witten, Electric-magnetic duality, monopole condensation, and confinement in N=2N=2 supersymmetric Yang--Mills theory , Nuclear Phys. B 426 (1994), 19--52. doi:10.1016/0550-3213(94)90124-4 (https://doi.org/10.1016/0550-3213(94)90124-4).DOI
  154. H. Shen, R. Zhu and X. Zhu, A stochastic analysis approach to lattice Yang--Mills at strong coupling , Comm. Math. Phys. 400 (2023), 805--851. doi:10.1007/s00220-022-04609-1 (https://doi.org/10.1007/s00220-022-04609-1).DOI
  155. S. G. Tankeev, On the standard conjecture of Lefschetz type for complex projective threefolds , Izv. Math. 74 (2010), 167--187. doi:10.1070/IM2010v074n01ABEH002484 (https://doi.org/10.1070/IM2010v074n01ABEH002484).DOI
  156. S. G. Tankeev, On the standard conjecture of Lefschetz type for complex projective threefolds. II , Izv. Math. 75 (2011), 1047--1062. doi:10.1070/IM2011v075n05ABEH002563 (https://doi.org/10.1070/IM2011v075n05ABEH002563).DOI
  157. T. Tao, The logarithmically averaged Chowla and Elliott conjectures for two-point correlations , Forum Math. Pi 4 (2016), e8. doi:10.1017/fmp.2016.6 (https://doi.org/10.1017/fmp.2016.6).DOI
  158. G. G. Turrigiano, K. R. Leslie, N. S. Desai, L. C. Rutherford and S. B. Nelson, Activity-dependent scaling of quantal amplitude in neocortical neurons , Nature 391 (1998), 892--896. doi:10.1038/36103 (https://doi.org/10.1038/36103).DOI
  159. T. Tao and J. Teräväinen, The structure of logarithmically averaged correlations of multiplicative functions, with applications to the Chowla and Elliott conjectures , Duke Math. J. 168 (2019), 1977--2027. doi:10.1215/00127094-2019-0002 (https://doi.org/10.1215/00127094-2019-0002).DOI
  160. T. Tao and J. Teräväinen, Odd order cases of the logarithmically averaged Chowla conjecture , J. Théor. Nombres Bordeaux 30 (2018), 997--1015. doi:10.5802/jtnb.1062 (https://doi.org/10.5802/jtnb.1062).DOI
  161. A. M. Turing, Computing machinery and intelligence , Mind 59 (1950), no. 236, 433--460. doi:10.1093/mind/LIX.236.433 (https://doi.org/10.1093/mind/LIX.236.433).DOI
  162. R. Taylor and A. Wiles, Ring-theoretic properties of certain Hecke algebras , Ann. of Math. (2) 141 (1995), no. 3, 553--572. doi:10.2307/2118560 (https://doi.org/10.2307/2118560).DOI
  163. T. H. Trinh, Y. Wu, Q. V. Le, H. He and T. Luong, Solving olympiad geometry without human demonstrations , Nature 625 (2024), no. 7995, 476--482. doi:10.1038/s41586-023-06747-5 (https://doi.org/10.1038/s41586-023-06747-5).DOI
  164. J. Uesato, N. Kushman, R. Kumar, F. Song, N. Siegel, L. Wang, A. Creswell, G. Irving and I. Higgins, Solving math word problems with process- and outcome-based feedback , preprint (2022). arXiv:2211.14275 (https://arxiv.org/abs/2211.14275).arXiv
  165. M. Varesco, Hodge similarities, algebraic classes, and Kuga--Satake varieties , Math. Z. 305 (2023), 69. doi:10.1007/s00209-023-03390-8 (https://doi.org/10.1007/s00209-023-03390-8).DOI
  166. L. R. Varshney, B. L. Chen, E. Paniagua, D. H. Hall and D. B. Chklovskii, Structural properties of the Caenorhabditis elegans neuronal network , PLoS Comput. Biol. 7 (2011), e1001066. doi:10.1371/journal.pcbi.1001066 (https://doi.org/10.1371/journal.pcbi.1001066).DOI
  167. M. Viazovska, The sphere packing problem in dimension 8 , Ann. of Math. (2) 185 (2017), no. 3, 991--1015. doi:10.4007/annals.2017.185.3.7 (https://doi.org/10.4007/annals.2017.185.3.7).DOI
  168. A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, Ł. Kaiser and I. Polosukhin, Attention is all you need , Advances in Neural Information Processing Systems 30 (2017). arXiv:1706.03762 (https://arxiv.org/abs/1706.03762).arXiv
  169. A. Wald, Sequential tests of statistical hypotheses , Ann. Math. Statist. 16 (1945), no. 2, 117--186. doi:10.1214/aoms/1177731118 (https://doi.org/10.1214/aoms/1177731118).DOI
  170. S. Weir, obsidian-brain , server for semantic search and graph analysis of an Obsidian vault, npm package, version 1.7.24 (2026). sweir1.github.io/obsidian-brain (https://sweir1.github.io/obsidian-brain/).link
  171. A. Weil, Number Theory: An Approach through History from Hammurapi to Legendre , Birkhäuser, Boston, 1984. doi:10.1007/978-0-8176-4571-7 (https://doi.org/10.1007/978-0-8176-4571-7).DOI
  172. H. W. Watson and F. Galton, On the probability of the extinction of families , J. Anthropol. Inst. Great Britain and Ireland 4 (1875), 138--144. doi:10.2307/2841222 (https://doi.org/10.2307/2841222).DOI
  173. A. Wiles, Modular elliptic curves and Fermat's Last Theorem , Ann. of Math. (2) 141 (1995), no. 3, 443--551. doi:10.2307/2118559 (https://doi.org/10.2307/2118559).DOI
  174. E. Witten, Quantum field theory and the Jones polynomial , Comm. Math. Phys. 121 (1989), 351--399. doi:10.1007/BF01217730 (https://doi.org/10.1007/BF01217730).DOI
  175. H. Wang, M. Unsal, X. Lin, M. Baksys et al., Kimina-Prover Preview: towards large formal reasoning models with reinforcement learning , preprint (2025). arXiv:2504.11354 (https://arxiv.org/abs/2504.11354).arXiv
  176. J. Wei, X. Wang, D. Schuurmans, M. Bosma, B. Ichter, F. Xia, E. Chi, Q. Le and D. Zhou, Chain-of-thought prompting elicits reasoning in large language models , Advances in Neural Information Processing Systems 35 (2022). arXiv:2201.11903 (https://arxiv.org/abs/2201.11903).arXiv
  177. K. Yang, A. M. Swope, A. Gu, R. Chalamala et al., LeanDojo: theorem proving with retrieval-augmented language models , Advances in Neural Information Processing Systems 36 (2023), Datasets and Benchmarks Track. arXiv:2306.15626 (https://arxiv.org/abs/2306.15626).arXiv
  178. A. Yang, B. Zhang, B. Hui, B. Gao, B. Yu, C. Li et al., Qwen2.5-Math technical report: toward mathematical expert model via self-improvement , preprint (2024). arXiv:2409.12122 (https://arxiv.org/abs/2409.12122).arXiv
  179. Z. Zhang, A. Delaval, L. Chen, J. Chen, J. Xu, Y. Liao, J. Jiang, C. Liu and B. Dong, An AI-assisted formalization of the Poincaré conjecture , preprint (2026). arXiv:2610.08329 (https://arxiv.org/abs/2610.08329).arXiv
  180. R. Zippel, Probabilistic algorithms for sparse polynomials , in Symbolic and Algebraic Computation (EUROSAM '79), Lecture Notes in Comput. Sci. 72, Springer, Berlin, 1979, 216--226. doi:10.1007/3-540-09519-5_73 (https://doi.org/10.1007/3-540-09519-5_73).DOI
  181. E. Zelikman, Y. Wu, J. Mu and N. D. Goodman, STaR: bootstrapping reasoning with reasoning , Advances in Neural Information Processing Systems 35 (2022). arXiv:2203.14465 (https://arxiv.org/abs/2203.14465).arXiv

Version history

  1. v1Submitted by Deep BhattacharjeeInitial depositCurrentOct 19, 2026