AI4math 信息站
人工智能与数学交叉领域的前沿信息平台
AI4Math Hub · Papers, tools, and resources for AI4Math
Latest Papers
- ICLR 2026 Representation Learning for Mathematics
- Gemma 3: Google's Latest Open Model with Strong Math Reasoning
- Claude 3.7 Sonnet: Extended Thinking for Complex Reasoning
- mathlib4 reaches 5 million lines of code
- LLMlean 2.0: Enhanced Lean 4 Integration with LLMs
- DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning
- Qwen2.5-Max: Advanced multimodal reasoning at scale
- OpenAI o3: Breakthrough in mathematical reasoning and code generation
- Kimina-Prover
- Gemini 2.0 Flash Thinking: Multimodal reasoning with implicit chain-of-thought
- ProofWidgets 2.0: Interactive Proof Visualization for Lean
- NeurIPS 2025 AI4Math Highlights
- Frenzy Math Launches AI Tutor for AMC 10/12 Preparation
- TheoremLLaMA: Transforming General-Purpose LLMs into Lean4 Experts
- xAI Grok 3: Reasoning Model with Strong Math Capabilities
- Frenzy Math Report: AI Tutoring Improves Competition Scores by 40%
- Lean 4.9: Enhanced Performance and User Experience
- Frenzy Math Series A Funding: $12M to Scale AI Math Education
- Stephen Wolfram on AI and the Future of Mathematics
- IMO 2025: AI Systems Achieve Silver Medal Performance
- ICML 2025 Mathematical Reasoning Track
- AAAI 2025 AI for Mathematics
- Kimi k1.5: Scaling Reinforcement Learning with LLMs
- Terence Tao: 10-Minute Short Talk on Formalization and AI
- IMO 2024 Grand Challenge: Progress Report
- Qwen2.5-Math: The world's leading mathematical LLM
- AlphaProof: Neuro-symbolic theorem proving at the olympiad level
- Mathematical Proof Verification Using Machine Learning
- NuminaMath-CoT: China's open mathematical reasoning model
- Formal Verification of Neural Networks
- Towards Large Language Models as Copilots for Theorem Proving
- Terence Tao on AI and the Future of Mathematical Research
- DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models
- Aya: An Open Science Initiative to Democratize AI
- Solving Olympiad Geometry without Human Demonstrations
- Matthew Wiener on the Future of AI and Mathematics
- The Cantor Attic: A Database of Mathematical Cardinality
- Naïve Type Theory by Thorsten Altenkirch
- FunSearch: Making new discoveries in mathematical sciences with Large Language Models
- Kevin Buzzard: The Xena Project and Formalizing Undergraduate Mathematics
- MMMU: A Massive Multi-discipline Multimodal Understanding and Reasoning Benchmark
- Transformer-Based Models for Automated Theorem Proving
- Timothy Gowers: The Intersection of AI and Mathematical Collaboration
- LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
- Learning to Reason in Large Language Models via Process Reward Models
- Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
- Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
- A Complete Proof of the Liquid Tensor Experiment
- Formal Mathematics Statement Curriculum Learning
- Solving Quantitative Reasoning Problems with Language Models
- HTPS: HyperTree Proof Search for Neural Theorem Proving
- A Generalist Neural Theorem Prover
- Autoformalization with Large Language Models
- MiniF2F: A Cross-System Benchmark for Formal Olympiad-Level Mathematics
- GPT-f: Generative Language Modeling for Automated Theorem Proving
Resources
25 companies · 22 projects · 3 tools