Math 5810: Special Topics in Mathematics
Math and AI
Fall 2026 · University of Colorado Boulder
Monday, Wednesday, Friday 1:25–2:15 pm · Mathematics Building, Room 350
Course Zoom link ↗
Instructors:
Agnès Beaudry · Mathematics 312 · office hours Mondays & Tuesdays, 11:00 am–12:00 pm
Katherine E. Stange · Mathematics 308
Jonathan Wise · Mathematics 204
Spotify playlist ↗ Suggestions welcome
- Class schedule ↗day by day: lectures, Friday seminar talks, and what is due
- Syllabus
- Set-up instructions for vibecoding
- AI use rules — for the department's AI access (gateway key, gateway chat, departmental subscriptions); read before using them
- Math of LLMs lectures
- Kate's AI Reading List
Course plan
Four thematic units, each culminating in a concrete project:
- Theory of LMs. How language models work: tokens, context, transformers, training — and the distinction between amodel and the broader AI system built around it.Project: build a small language model in Python.
- AI-assisted research. Using AI tools for mathematical work: vibe-coding, vibe-proofing, agents, and harnesses.Projects: vibe-coding visualizations; AI-assisted research paper; class-built harness.
- Formalization. Introduction to formalization languages — Lean — and proof assistants for verification.Projects: formalization of research paper; add formalization harness.
- Ethical practices. Issues surrounding AI in mathematical research: data sources, bias, resources, environmental cost, verification, responsibility, disclosure, reproducibility, attribution, and consequences for mathematicians.Project: class written guidelines for responsible AI use in research.
Vibecoding
Using AI to write, test, and understand mathematical code.
- Set-up instructions for vibecoding — todo before we start
- Python Primer — a from-scratch, ~90-minute introduction to Python for mathematicians who have never programmed
- Building and Publishing a Visualization with Codex — a course guide: the full workflow from prompt to published page, worked end to end
- Slop Is a Skill Issue: The Engineering Around Coding Agents — Thomas Dietert (Mercury) in MIT's Agentic Coding in Practice seminar, on context engineering, harness engineering, and backpressure — a video file; the slides are alongside it
- Learning Opportunities — Cat Hicks's Claude and Codex skill: after a piece of architectural work, it offers a short prediction or retrieval exercise, so the human is still learning while the machine writes the code
- CSCI 2830: Build with AI — a full CU Boulder course on building with AI, running concurrently this semester
Math of LLMs
What is a large language model?
- The Mathematics of Large Language Models — an eight-lecture mini-course with a build-your-own-LLM project, by Agnès Beaudry and Katherine E. Stange
Lean
Formalizing mathematics with the Lean proof assistant.
- Lean — the language and proof assistant itself, with the install instructions
- The Lean FRO — the Lean Focused Research Organization — the nonprofit that develops Lean itself; about, team, and roadmap
- The Lean community — the hub: Mathlib, tooling, and where to start
- Mathlib — the single monolithic library of formalized mathematics everything builds on
- The Natural Number Game — build the naturals from the Peano axioms in your browser
- Mathematics in Lean — Avigad and Massot's tutorial book, written for mathematicians
- Theorem Proving in Lean 4 — the reference text on the type theory underneath
- Lean Zulip — where the community actually talks; beginners' questions are welcome
- Fermat's Last Theorem in Lean — Kevin Buzzard's multi-year, multi-author project at Imperial to formalize FLT
- The Equational Theories Project — Tao, Monticone, and Srinivas: 4,694 laws of magmas and 22 million implications between them, settled by humans and automated provers together and checked in Lean
- The polynomial Freiman–Ruzsa conjecture — a 2023 theorem formalized within weeks of the paper
AI-Assisted Research
Tools for doing mathematics with agents, and the benchmarks and challenges that measure how far they get.
- Numina Studio — Project Numina's workspace for long-running Claude agents · overview: Jia Li's demo at IHES, on video
- Danus — orchestrates a swarm of proving agents behind a verifier and a fact-graph memory (Frenzy Math; arXiv 2607.06447)
- mathcity — a Gas City pack for mathematics research: agents do the work and file briefs, humans adjudicate
- The First Proof Project — testing AI with human research problems
- IMProofBench — ETH's research-level proof benchmark: private PhD-level problems, public leaderboard (arXiv 2509.26076)
- The Ramanujan Challenge — prove formulas for π, e, and values of ζ — a research-level test of AI systems, run in July 2026
- Benchmarks in Leipzig — 100 research-level problems with known answers, compiled by 49 mathematicians at MPI MiS (arXiv 2606.05818)
Ethics
It's complicated.
- The Leiden Declaration on Artificial Intelligence and Mathematics — fifteen mathematicians out of a 2025 Lorentz Center workshop, endorsed by the International Mathematical Union and signed by 3,500+: what proof, attribution, and peer review are for, and what AI puts at risk
- On the Dangers of Stochastic Parrots: Can Language Models Be Too Big? — Bender, Gebru, McMillan-Major, and Shmitchell at FAccT 2021 — the paper that set the terms of the argument
- The real energy use of agentic AI — Zeke Hausfather measures his own coding agent — about 150 Wh per prompt, some 600 times a chatbot answer, and roughly a tenth of a US household's electricity over a year
- Catching Crumbs from the Table — SciFi: Ted Chiang in Nature, from 2000.
- Machine-Assisted Proof — Terence Tao in the Notices of the AMS, on what proof assistants and machine learning do for the working mathematician
- Proofs and Prompts — a communal blog on how AI is changing mathematical practice
- The AI Village — frontier agents with their own computers, pursuing long-horizon goals together, every weekday since April 2025
- AI 2040: Plan A — a plan for delaying superintelligence to 2040
- Pessimists Archive — historical hysteria that greeted electricity, bicycles, elevators, radio, ...
Resources
Models and compute. Anything the Department of Mathematics provides — the gateway key, the departmental chat, departmental subscriptions — is covered by the AI use rules; read them first.
- AI use rules — the three rules for using the department's AI access (gateway key, gateway chat, departmental subscriptions) — your usage is not private; delete old chats; no sharing, model-improvement, connectors, or plug-ins
- Github — More powerful without university login, but there are some non-CU education benefits to signing up for https://github.com/education
- Google Gemini through CU — Identikey login
- ChatGPT Edu through CU — Identikey login: approved model for sensitive university information; very limited quota
- CU AI Chat — Identikey login: the department's own interface to the mainstream LLMs, and the gateway for Claude Code and Codex; pay per token. Subject to the AI use rules above
- CU AI Tools List — the campus catalogue of vetted AI tools — productivity, coding, and data analysis — with the data classification each one is approved for
- Google Colab — Identikey login: free GPU notebooks in the browser, with Gemini built in as a coding copilot
- Hugging Face model hub — hundreds of thousands of open-weight models, filterable by task and size, most of them free to download and run
- The NAIRR Pilot — NSF-led access to supercomputers, datasets, and model credits