Sister section
ProofsPath
Olympiad-style proof techniques: AM-GM, Cauchy-Schwarz, induction, extremal principle, and more — paired with cross-links to the Lean-verified counterparts in the main TheoremPath manifest.
TheoremPath is the parent network for the rigorous machine-learning curriculum this section borrows from.
Flagship
Flagship · 45 min
A Worked Lean Proof Tour — Hoeffding's Finite-Sum Bound
A line-by-line walkthrough of an actual FormalSLT Lean file. Starts from the paper statement, names every Mathlib lemma invoked, explains why each tactic is the right choice at its position, and ends at the kernel-checked QED. The reference for what a finished, audited Lean proof looks like.
Flagship · 11 min
Induction — Strong vs Weak
Mathematical induction in two flavors. Weak (ordinary) induction proves $P(n+1)$ from $P(n)$. Strong induction proves $P(n+1)$ from $P(1), P(2), \ldots, P(n)$. They are logically equivalent over the natural numbers, but problems naturally fit one or the other. Cue for strong: 'I need the property at multiple smaller values, not just the immediate predecessor.' Pairs with well-ordering and infinite descent.
Flagship · 11 min
Invariants and Monovariants
An invariant is a quantity preserved by the moves of a process; a monovariant strictly decreases (or increases) with each move. Together they prove non-reachability (invariants) and termination (monovariants). Cue: 'process / game / configuration changes by allowed moves.' The technique behind the 15-puzzle parity argument and many olympiad combinatorics problems.
Flagship · 30 min
Lean 4 Essentials for Mathematicians
The pieces of Lean 4 you actually use when writing a proof: types, propositions, terms, tactics, the kernel, and the trust boundary. Targeted at mathematicians and ML theorists coming from paper proofs; assumes no functional-programming background.
Flagship · 12 min
Modular Arithmetic Essentials for Contests
Modular arithmetic as the language of contest number theory. Equivalence relations $\bmod n$, sound operations (addition, multiplication, exponentiation), unsound operations (cancellation without coprimality), modular inverses when $\gcd(a, n) = 1$. The toolkit on which Fermat, Euler, Wilson, CRT, LTE, and quadratic residues all build.
Flagship · 30 min
Navigating Mathlib4
How to find the right lemma in a 1.6-million-line library. The naming convention, the search tactics (`exact?`, `apply?`, `rw?`, `library_search`), the file structure, and the operational habit of finding lemmas instead of re-proving them. The hardest skill for new Mathlib contributors and the most useful one to develop early.
Flagship · 11 min
Pigeonhole Principle (Elementary Applications)
If n+1 objects are placed in n boxes, some box has at least two objects. The simplest non-trivial counting argument and the entry point to Ramsey-style combinatorics. Cue: 'finite set forced to have a coincidence.' Worked applications from IMO 1985, IMO 1972, and the classical 'two people in NYC with the same number of hairs' family.
Flagship · 10 min
Proof by Contradiction
Assume the negation, derive a contradiction, conclude the original statement. The most flexible non-constructive technique in the proof writer's toolkit. Cue: 'suppose, for contradiction, that...' Pairs with the law of excluded middle, infinite descent, and proofs of irrationality and infinitude.
Flagship · 25 min
Sorry-Free Discipline and Axiom Auditing in Lean 4
How to keep a Lean codebase trustworthy: ban `sorry`, audit axioms with `#print axioms`, gate the CI on both. The operational practices that make 'kernel-checked' a meaningful claim in a project with hundreds of theorems.
Flagship · 20 min
Tactic Mode vs Term Mode in Lean 4
When to construct a proof term directly and when to use tactics. The two modes produce the same kernel-checked artifact; the choice is about readability and authoring ergonomics. Rule of thumb: term mode for one-liners and definitions, tactic mode for anything with cases or substantial rewriting.
Flagship · 12 min
The AM-GM Inequality
The arithmetic mean of $n$ non-negative reals is at least their geometric mean, with equality iff all are equal. The most-used inequality in olympiad mathematics, with multiple proofs (Cauchy's reverse induction, smoothing, Jensen). Cue: products and sums that should balance, optimization with multiplicative structure. Pairs with Cauchy-Schwarz, power-mean, Jensen.
Flagship · 12 min
The Cauchy Functional Equation
The functional equation f(x+y) = f(x) + f(y). On Q every solution is f(x) = cx. On R the additional regularity conditions (continuity at one point, monotonicity on an interval, boundedness on a set of positive measure, measurability) all force the same answer; without any regularity, pathological non-linear solutions exist via a Hamel basis. The canonical first functional equation, gateway to the entire technique.
Flagship · 12 min
The Cauchy-Schwarz Inequality
$\left(\sum a_i b_i\right)^2 \le \left(\sum a_i^2\right)\left(\sum b_i^2\right)$ with equality iff one sequence is a scalar multiple of the other. The bilinear backbone of olympiad inequalities. Multiple proofs (discriminant, Lagrange identity, Engel/Titu form). Cue: products of sums, sums of products, ratios with squares. Pairs with AM-GM, Schwarz inner-product geometry, the rearrangement inequality.
Flagship · 25 min
The Curry-Howard Correspondence
Propositions are types; proofs are programs; proof composition is function application. The structural identity between logic and computation that makes dependent-type-theory proof assistants like Lean possible. Page covers the basic translation, intuitionistic vs classical reading, and the operational consequences.
Flagship · 11 min
The Extremal Principle
Consider the largest, the smallest, the extremal element. The extremal principle says that in any finite or well-ordered set, an extremal element exists, and its extremality often forces the conclusion. Cue: 'consider the maximum / minimum / longest / shortest...' Pairs with monovariants and well-ordering.
Flagship · 9 min
The Well-Ordering Principle
Every non-empty subset of the natural numbers has a least element. The principle that powers smallest-counterexample arguments, the division algorithm, and infinite descent. Equivalent to mathematical induction over $\mathbb{N}$. Cue: 'consider the smallest...' Pairs with induction, infinite descent, and the extremal principle.
Flagship · 13 min
Vieta Jumping
A descent technique for Diophantine and number-theoretic problems where Vieta's formulas on a quadratic let you swap one root for the other and shrink a witness pair to derive a contradiction. The canonical solution to IMO 1988 Problem 6 - 'if ab+1 divides a^2+b^2, the quotient is a perfect square' - and a Putnam-style toolkit for two-variable integer problems with a hidden quadratic.