NeurIPS 2026, Atlanta Hall C3, Saturday, December 12, 2026

Accepted Papers

  1. Cost-Effective Automated Judging of Natural-Language Mathematical Proofs [paper]
  2. Cross-Engine Admission Contracts for Autonomous Formalization [paper]
  3. Learner History and Calibration for Generated Mathematics Questions [paper]
  4. Where Induction Runs Out: Description-Length Difficulty and the Memorisation Gap in Integer-Sequence Benchmarks [paper]
  5. Discovery of 6 New Zarankiewicz Numbers via LLM-guided Evolutionary Search [paper]
  6. LLMs Under-Detect Circular Reasoning in Mathematical Handoffs [paper]
  7. Can an AI Agent Rediscover a Blaschke-Curve Invariant? [paper]
  8. Formalize, Don't Optimize: The Heuristic Trap in LLM-Generated Combinatorial Solvers [paper]
  9. Feedback Aliasing in Lean Repair Loops: A Controlled Intervention Study [paper]
  10. SURGE: Sparse Update Routing via Gated Entropy for Efficient Active Distillation [paper]
  11. VisTIRA: Closing the Image–Text Modality Gap in Visual Math Reasoning via Structured Tool Integration [paper]
  12. Automated conjecture resolution with formal verification [paper]
  13. Reasoning Depth Erodes the Premise Verification That Post Training Builds [paper]
  14. Correlated Criteria Drive Reward Over-Optimization: Redundancy-Aware Scheduling for Checklist Rewards [paper]
  15. OrthogonalAgent: An Auditable Control Layer for Agentic Statistical Reasoning [paper]
  16. Beyond Compilation: Human-Calibrated Evaluation of Semantic Faithfulness in Lean Autoformalization [paper]
  17. An Agentic Bug-Hunt in SymPy [paper]
  18. Drop the Act: Probe-Filtered RL for Faithful Chain-of-Thought Reasoning [paper]
  19. The Errors Reviewers Catch: Statement-Level Autoformalization Errors and What Frontier Models Miss [paper]
  20. SEMINAR: Synchronization Engine for Mathematical Illustration, Narration, and Reasoning [paper]
  21. PartialMap Ledger: When Mathematical Agents May Reuse Tool Receipts [paper]
  22. Failure-Driven Verification in Human–AI Mathematics: An Explicit K3 Case Study [paper]
  23. Preserving Mathematical Reasoning in Compressed Diffusion Language Models via Trajectory-Aware Low-Rank Approximation [paper]
  24. Machine-Checked Formalization of the HHL and QSVT Quantum Algorithms in Lean 4 [paper]
  25. Do Mathematical LLMs Survive Analog Inference? [paper]
  26. Dependency Distance Audits Descendant Leakage in Lean Proving Benchmarks [paper]
  27. Claim-Centered Research Records for AI-Assisted Theoretical Research [paper]
  28. Nudging Beyond the Comfort Zone: Efficient Strategy-Guided Exploration for RLVR [paper]
  29. ClaimScope: Label-Blind Witness Verification for Mathematical Claim Auditing [paper]
  30. When Logical Information Emerges: Recoverability, Behavioral Expression, and Representation Stability in Language Models [paper]
  31. Learning State Transitions Improves Downstream Policy Learning in Geometry Theorem Proving [paper]
  32. The Shape of Mathematical Creativity: Measuring Mathematical Exploration in Formal Proof Generation [paper]
  33. Learning to Discover Interesting Mathematics [paper]
  34. ParaLLax: Disentangling Difficulty from Validity in Reasoning Verifiers [paper]
  35. Budget Boundary Effects in Test-Time Mathematical Reasoning [paper]
  36. When Tools Lie: Reliability of Mathematical Agents Under Corrupted Tool Feedback [paper]
  37. Beyond the Compile Check: Separating False from Unproven in LLM Conjecture Generation [paper]
  38. When Does Variance Reduction Help GRPO? A CRN Case Study in Mathematical Reasoning [paper]
  39. FLOWEDIT: Information-Theoretic Set-Valued Mathematical Reasoning under Conflicting Conditions [paper]
  40. The Problem Is the Problem: Towards Scalable Mathematical Discovery [paper]
  41. Viva La Vida: Verification and Accumulation Failures in Multi-Agent Proof Search [paper]
  42. Rediscover Before You Discover: A Recent Human Find as the Regression Target for an Agentic Geometry Pipeline [paper]
  43. Beyond Solve Rates: Harness Effects and Run-to-Run Variability in Agentic Theorem Proving [paper]
  44. Numina-Prover: Open-Source Vibe Proving for Informal Mathematics via Parallel Subagents [paper]
  45. Do Small Language Models Verify What They Can Solve? Synthetic Derivations with Planted Errors [paper]
  46. Dense Neuro-Symbolic Reasoning in a Unified Geometry State [paper]
  47. When the Calculator Lies: Mathematical Agents Defer to Faulty Tools Even When They Know Better [paper]
  48. HammerRank: Symbolic Learning-to-Rank Premise Selection for the Lean Hammer [paper]
  49. Improved Convergence Rates for Stochastic Multi-Gradient Descent: A Human-Verified AI Proof [paper]
  50. DoubtLess: Training-Free Contrastive Decoding for Efficient Mathematical Reasoning [paper]
  51. MathLoopBench: Evaluating Agentic Mathematical Discovery Loops [paper]
  52. Trees and Graphs with Non Log-concave Dominating Set Sequence via Patternboost [paper]
  53. Measuring and Mitigating Mode Collapse in RLVR [paper]
  54. A dataset of formalised theorem statements from the Annals of Mathematics [paper]
  55. Lea: An Agent Backbone for Mathematician-Controlled Formalization in Lean [paper]
  56. LeanPRM: Lean-Grounded Supervision for Natural Language Proof Verification [paper]
  57. FLMF: Verified Autoformalization of the Digital Library of Mathematical Functions [paper]
  58. LinAlg-Bench: A Benchmark Exposing Structural Failure Modes in LLM Linear Algebra - Where Models Stop Computing and Start Hallucinating [paper]
  59. Model-Dependent Transfer of Solver-Cost Orderings in SAT Evaluation [paper]
  60. Learning Where to Constrain: Meta-Learned Trust Allocation for Mathematical Reasoning [paper]
  61. A Guard-Aware Junk-Value Linter for Lean 4: Auditing Formal Benchmarks and Improving Autoformalization [paper]
  62. What Has Actually Been Proved? Auditable Paper-to-Lean Alignment with LeanTrail [paper]
  63. DUALITYCERT: Verifier-Gated Language-Model Repair of Broken Duality Claims in Quantum Field Theory [paper]
  64. Can Small Transformers Learn the Language of Coxeter Groups? [paper]
  65. Process Rewards with Learned Reliability [paper]
  66. Reliability-Aware Metacognitive Routing for Cost-Efficient Mathematical Reasoning [paper]
  67. Does a Frontier Large Language Model Know What It Can Solve? A 100-Conjecture Calibration Study [paper]
  68. Beyond Aggregate Accuracy: Shared Failures and Context Sensitivity in Lean Proof Completion [paper]
  69. Improving semantic equivalence in research-level math formalization [paper]
  70. Do Theorem Provers Need Theorem-Proving Agents? mini-Lean-agent: A Coding-Agent Baseline for Lean [paper]
  71. LLM-Guided Graph Construction with Elite-Seeded Local Search: Improved Lower Bounds for the Degree-Diameter Problem [paper]
  72. Order-Invariant Answers, Order-Sensitive Representations in Mathematical Reasoning [paper]
  73. Escaping the Token-by-Token Learning Trap in On-Policy Distillation for Mathematical Reasoning [paper]
  74. BruKnot: Learning Verifiable Constructions in the Reidemeister Graph [paper]
  75. The Verification Gap: Auditing Proof Progress and Repair on IMO 2026 [paper]
  76. Knowing Before Saying: Internal Correctness Signals in Mathematical Reasoning [paper]
  77. Language Models Under False Lean 4 Reports: Initial Decisions and Final Proofs [paper]
  78. Proof Perplexity: A Probabilistic Approach to Measuring non-triviality in Machine Generated Proofs [paper]
  79. GeoGenBench: Symbolically Verified Generation of Geometry Diagrams [paper]
  80. When Sharp Layer Bounds Cannot Coexist: Exact Antichain Saturation via Symbolic Search [paper]
  81. Prove2Me: An Open Collaborative Platform for Scaling Math Formalization [paper]
  82. When Is Proof-Step Verification Worth Its Cost? Operating Requirements of Certify-or-Decline Verification for Open-Weight Mathematical Reasoning [paper]
  83. Accuracy, Confidence, and Sample Budgets: Exact Certificates for Mathematical Benchmark Claims [paper]
  84. Query–Key Ensembles for Mathematical Reasoning Verification [paper]
  85. Studying the Effects of Task Diversity Using Small Mathematical Worlds [paper]
  86. MMGO-Bench: A Multimodal Graph Optimization Benchmark [paper]
  87. Improving Math Reasoning through Value-Guided Informative Search [paper]
  88. Sparse coloring for isosceles-free grids: an AI-assisted proof case study [paper]
  89. StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean [paper]
  90. PeerConf: Self-Calibrating Early Stopping for Efficient Parallel LLM Reasoning [paper]
  91. On the Off-Policy Teacher in On-Policy Distillation [paper]
  92. Agentic Computational Algebra [paper]
  93. When Group Normalization Undermines Sparse Reward Auditing in RLVR [paper]
  94. Productive Failure in Agentic Mathematics: An Auditable Connected-Domination Case Study [paper]
  95. ConjectureLineage: Learning Mathematical Taste from Documented Follow-Up [paper]
  96. Does My Embedding Reflect That \(A = B\)? Evaluating Mathematical Equivalence in Embedding Models [paper]
  97. When Does Long Thinking Help? A Discovery- Execution Framework for Mathematical Reasoning [paper]
  98. EULER: Searching Representation–Operation Pairs for Mathematical Discovery [paper]
  99. An Automated Theorem Proving System and Visualized Lean Library for Sampling Theory, Optimisation and Geometry [paper]
  100. MathAtlas: A Benchmark for Autoformalization in the Wild [paper]
  101. Permissiveness Credit: What Formal Math Benchmarks Reward Besides Capability [paper]
  102. Encouragement as Pedagogy: Using AI-Mediated Mathematical Participation to Address Math Anxiety in Education and Outreach [paper]
  103. Proving at Scale for Universal Algebra [paper]
  104. Detecting and Correcting Reasoning Failures: A Controlled Negative Result for a Residual-Stream Monitor [paper]
  105. Attention-Graph Curvature for the Verification of Mathematical Reasoning [paper]
  106. Bolzano: From Expert-Guided Proof Search to Automated Open-Problem Solving [paper]
  107. Structural Coverage: Do AI Provers Use Mathlib the Way Mathematicians Do? [paper]
  108. AutoformBench: A Lean Formalization Benchmark for Advanced Mathematics [paper]
  109. Zero: A Meta-Agent for Mathematical Research [paper]
  110. Auditing LLM Program Search for Bermudan Stopping with Primal--Dual Certificates [paper]
  111. Verifiable Mathematical Reasoning as a Probe of Emergent Global Workspaces [paper]
  112. Automated Review of Mathematical Papers: Errors Found and Repaired in the Top Four Journals [paper]
  113. Basis Artifacts in Solution-Level Verification of LLM-Generated Linear Programs [paper]
  114. Learning Posterior Teachers for On-Policy Distillation [paper]
  115. Sage-to-Lean: Formal Verification of Answers from CAS-Augmented Mathematical Agents [paper]
  116. Evidence Integration in Large Language Models [paper]
  117. Beyond Solver Acceptance: Auditing Autoformalized Biomedical Claims [paper]
  118. VALG: An Agentic System for ML Theory Research [paper]
  119. Theorem Evolution Graphs: A Structured Representation of How Mathematical Theorems Build on One Another [paper]
  120. Human–AI Collaboration in Mathematics: A Practical Account [paper]
  121. Coding Agents for Coding Theory [paper]
  122. AxiomShift: Altering Axioms to Evaluate LLM Reasoning at Knowledge Boundaries [paper]
  123. Mitigating Reward Hacking in Mathematical Reasoning Without Ground-Truth Labels [paper]
  124. Searching for Graph Counterexamples with Mixed-Extension Templates [paper]
  125. AlphaApollo: A System for Deep Agentic Reasoning [paper]
  126. AlphaDiana: A System for Evaluating Reasoning Agents [paper]
  127. Agentic Algorithm Design: LLMs that Propose, Formalise, and Prove Runtime Bounds for Evolutionary Algorithms in Lean [paper]
  128. LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs [paper]
  129. Symbolic Search Is Not Exhausted: Persistent Proof-Space Exploration in Lean4 [paper]

The list of accepted papers can also be found on OpenReview.

Reviewers

We thank the following reviewers for helping make the workshop possible (names are listed in alphabetical order by full name):