{"total":30,"rows":[{"id":"2605.00674","title":"Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs","created":"2026-05-01","cited_by_count":137,"area":null},{"id":"2606.05400","title":"LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization","created":"2026-06-03","cited_by_count":12,"area":null},{"id":"2603.19329","title":"Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification","created":"2026-03-18","cited_by_count":11,"area":null},{"id":"2605.13137","title":"LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving","created":"2026-05-13","cited_by_count":10,"area":null},{"id":"2605.13171","title":"Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics","created":"2026-05-13","cited_by_count":10,"area":null},{"id":"2605.29955","title":"Formalizing Mathematics at Scale","created":"2026-05-28","cited_by_count":10,"area":null},{"id":"2603.15929","title":"Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium","created":"2026-03-16","cited_by_count":9,"area":null},{"id":"2606.29493","title":"Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving","created":"2026-06-28","cited_by_count":9,"area":null},{"id":"2608.28433","title":"Prove2Me: An Open Collaborative Platform for Scaling Math Formalization","created":"2026-08-28","cited_by_count":5,"area":null},{"id":"2512.14252","title":"G\\\"odel's Poetry","created":"2025-12-16","cited_by_count":1,"area":null},{"id":"2603.04528","title":"Discovering mathematical concepts through a multi-agent system","created":"2026-03-04","cited_by_count":1,"area":null},{"id":"2605.19063","title":"Mapping Uncharted Symmetries: Machine Discovery in Combinatorics","created":"2026-05-18","cited_by_count":1,"area":null},{"id":"2606.13782","title":"MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis","created":"2026-06-11","cited_by_count":1,"area":null},{"id":"2607.07779","title":"From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier","created":"2026-07-08","cited_by_count":1,"area":null},{"id":"2609.05157","title":"AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics","created":"2026-09-04","cited_by_count":1,"area":null},{"id":"2601.16172","title":"Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study","created":"2026-01-22","cited_by_count":0,"area":null},{"id":"2603.20405","title":"Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP","created":"2026-03-20","cited_by_count":0,"area":null},{"id":"2604.17229","title":"Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1","created":"2026-04-19","cited_by_count":0,"area":null},{"id":"2604.21187","title":"Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery","created":"2026-04-23","cited_by_count":0,"area":null},{"id":"2605.06184","title":"Teaching LLMs Program Semantics via Symbolic Execution Traces","created":"2026-05-07","cited_by_count":0,"area":null},{"id":"2605.20120","title":"Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem","created":"2026-05-19","cited_by_count":0,"area":null},{"id":"2607.17388","title":"Mathematical Discovery in the Wild: AI-Guided Proofs in Banach Space Theory","created":"2026-07-19","cited_by_count":0,"area":null},{"id":"2609.34460","title":"When Does Structured Knowledge Help Neural Theorem Proving?","created":"2026-09-28","cited_by_count":0,"area":null},{"id":"2609.36663","title":"GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research","created":"2026-09-29","cited_by_count":0,"area":null},{"id":"2609.38384","title":"LeanPolish: Verified Supervision for Lean Proof Compression","created":"2026-09-29","cited_by_count":0,"area":null},{"id":"2609.39228","title":"Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization","created":"2026-09-30","cited_by_count":0,"area":null},{"id":"2610.09401","title":"Let the Library Speak: Self-Advertised Method Selection for Formal Proving","created":"2026-10-07","cited_by_count":0,"area":null},{"id":"2610.11862","title":"LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs","created":"2026-10-08","cited_by_count":0,"area":null},{"id":"2610.14059","title":"The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization","created":"2026-10-06","cited_by_count":0,"area":null},{"id":"2610.18089","title":"One-Sided Verification Under Limited Expert Review","created":"2026-10-13","cited_by_count":0,"area":null}],"next_cursor":null}