teorth/analysis
View on GitHub ↗ ★ 1,984 Lean
A Lean companion to Analysis I
4 mentions on Hacker News by 3 people: 0 stories, 4 comments · first 2025-07-30 · latest 2026-11-04
20082026
-
You can use Lean with Tao's book https://github.com/teorth/analysis If you've never used Lean try some of this https://hrmacbeth.github.io/math2001/ you will eventually just pick it up then can start understanding Mathlib abstract tactics.…
comment by hackermailman · 2026-11-04 · in Ask HN: Is AI good enough for math exercises? -
…In fact he has made lean4 versions of all of the proofs in his Analysis I textbook available here https://github.com/teorth/analysis He also has blogged about how he uses lean for his research. Edit to add: Looking at that repo, one thing…
comment by seanhunter · 2026-02-21 · in Lean 4: How the theorem prover works and why it's the new competitive edge in AI -
…a lot of progress. [1] eg https://youtube.com/playlist?list=PLs6rMe3K87LHu03WWh9rEbEhh... [2] https://github.com/teorth/analysis
comment by seanhunter · 2025-12-13 · in 50 years of proof assistants -
For now I'm just learning math with it! Currently I'm going through https://github.com/teorth/analysis (Tao's Lean companion to his textbook) and filling in the `sorry`s in the exercises (my solutions are in…
comment by danabramov · 2025-07-30 · in The Math Is Haunted