--- id: "/science-medicine/mathematics/" title: "mathematics: 20 curated resources" url: "https://skillissue.dev/science-medicine/mathematics/" --- # mathematics: 20 curated resources mathematics [Beginner](/science-medicine/beginner/index.md) [Intermediate](/science-medicine/intermediate/index.md) [Advanced](/science-medicine/advanced/index.md) [Expert](/science-medicine/expert/index.md) 20 resources · page 1 of 1 - ### [American Mathematical Society: use of AI policy](/frontier/research-feeds/american-mathematical-society-use-of-ai-policy/index.md) by [American Mathematical Society](https://ams.org/) American Mathematical Society policy on use of artificial intelligence in its journal publications. entity standard-policy US en - ### [DeepSeek-Prover](/frontier/research-feeds/deepseek-prover/index.md) by [DeepSeek](https://www.deepseek.com/) DeepSeek-Prover-V2 GitHub repo: Lean theorem proving models, ProverBench and download links. entity repo US en - ### [Goedel-Prover](/frontier/research-feeds/goedel-prover/index.md) by [Goedel-LM](https://github.com/Goedel-LM) Goedel-Prover-V2 GitHub repo: open-source language models for formal theorem proving in Lean. entity repo US en - ### [Harmonic (Aristotle)](/frontier/research-feeds/harmonic-aristotle/index.md) by [Harmonic](https://harmonic.fun/) Harmonic: company building Aristotle, an AI system for mathematical reasoning with formal proofs in Lean. entity lab US en - ### [Lean theorem prover](/frontier/research-feeds/lean-theorem-prover/index.md) by [Lean FRO](https://lean-lang.org/) Lean language site: open-source programming language and proof assistant for writing machine-checked mathematical proofs. entity repo Global en - ### [Lean community (mathlib)](/frontier/research-feeds/math-theorem-proving/index.md) by [leanprover-community](https://leanprover-community.github.io/) Lean community site: Lean theorem prover, the mathlib library and documentation. entity org Global en - ### [mathlib4](/frontier/research-feeds/mathlib4-repo/index.md) by [leanprover-community](https://leanprover-community.github.io/) mathlib4 GitHub repo: community mathematics library for Lean 4. entity repo Global en - ### [miniF2F](/frontier/research-feeds/minif2f/index.md) by [OpenAI](https://openai.com/) miniF2F GitHub repo from OpenAI: formal olympiad-level mathematics benchmark across several proof assistants. entity benchmark US en - ### [The Well (Polymathic AI)](/frontier/research-feeds/polymathic-ai-the-well/index.md) by [Polymathic AI](https://polymathic-ai.org/) Polymathic AI's The Well: about 15 TB of physics simulation datasets for training and benchmarking ML surrogate models. entity benchmark US en - ### [PutnamBench](/frontier/research-feeds/putnambench/index.md) by [Trishul: Trustworthy Intelligent Systems @ UT Austin](https://github.com/trishullab) PutnamBench GitHub repo: Putnam competition problems formalised in Lean, Isabelle and Coq for evaluating theorem-proving systems. entity benchmark US en - ### [AI achieves silver-medal standard solving International Mathematical Olympiad problems (Google DeepMind)](/frontier/research-feeds/deepmind-blog-ai-solves-imo-problems-at-silver-medal-level-2024/index.md) by [Google DeepMind](https://deepmind.google/) Google DeepMind post on AlphaProof and AlphaGeometry 2 reaching silver-medal level at IMO 2024. Beginner learning_resource guide UK en - ### [Mathematics for Machine Learning](/frontier/research-feeds/mathematics-for-machine-learning/index.md) by [mml-book](https://www.mml-book.com) Mathematics for Machine Learning book site by Deisenroth, Faisal and Ong, with free PDF on linear algebra, calculus and probability. Beginner learning_resource guide UK; Australia; international en - ### [MIT 18.06 Linear Algebra (Strang)](/frontier/research-feeds/mit-18-06-linear-algebra-strang/index.md) by [MIT OpenCourseWare](https://ocw.mit.edu/) MIT OpenCourseWare 18.06 Linear Algebra by Gilbert Strang, with video lectures, notes and problem sets. Beginner learning_resource course US en - ### [AI achieves silver-medal standard solving International Mathematical Olympiad problems (AlphaProof)](/frontier/research-feeds/alphaproof/index.md) by [Google DeepMind](https://deepmind.google/) Google DeepMind post on AlphaProof and AlphaGeometry 2 solving International Mathematical Olympiad problems at silver-medal level. Intermediate learning_resource blog US en - ### [Datawhale pumpkin-book 南瓜书](/frontier/research-feeds/datawhale-pumpkin-book/index.md) by [Datawhale](https://datawhale.cn) Datawhale Pumpkin Book: Chinese companion with step-by-step derivations of the formulas in Zhou Zhihua's Machine Learning textbook. Intermediate learning_resource book China zh - ### [Equational Theories Project (Tao et al.)](/frontier/research-feeds/equational-theories-project-tao-et-al/index.md) by [teorth](https://github.com/teorth) Terence Tao's Equational Theories Project: crowdsourced and automated-prover mapping of implications between equational laws. Intermediate learning_resource guide US/Global en - ### [Mathlib overview](/frontier/research-feeds/mathlib-overview/index.md) by [leanprover-community](https://leanprover-community.github.io/) Mathlib overview page mapping which areas of mathematics are formalised in the Lean mathlib library. Intermediate learning_resource docs Global en - ### [AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms](/frontier/research-feeds/alphaevolve/index.md) by [Google DeepMind](https://deepmind.google/) Google DeepMind post on AlphaEvolve, a Gemini-based coding agent that evolves algorithms for maths and computing problems. Advanced learning_resource blog West en - ### [Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning (AlphaProof)](/frontier/research-feeds/alphaproof-google-research-publication-page/index.md) by [Google Research](https://research.google/) Google Research publication on AlphaProof: olympiad-level formal mathematical reasoning with reinforcement learning. Advanced learning_resource paper UK/US en - ### [MaxProof](/frontier/research-feeds/maxproof/index.md) by [Jiacheng Chen et al. (Chinese University of Hong Kong)](https://www.cuhk.edu.hk/) arXiv paper (2026) introducing MaxProof, generative-verifier RL and test-time scaling for mathematical proofs. Advanced learning_resource paper China en [Plain-text Markdown copy](/science-medicine/mathematics/index.md)