[AntoineduFresne]

This PR brings in the randomized-algorithm framework of my master's thesis, Analysis of Randomised Algorithms in Lean 4 (ETH Zürich, 2026), with its nine case studies. Karger's minimum cut is one of them. The code comes in as it is, and we refactor afterwards.

• Thesis (PDF): https://github.com/AntoineduFresne/Master-Thesis/blob/b964d9ef3d30471841814f0d42ffb391e78ff2a4/docs/Analysis_of_Randomised_Algorithms_in_Lean4.pdf
• Original repository: https://github.com/AntoineduFresne/Master-Thesis. The Lean code is that of commit 765761e, the commit the thesis cites. DESIGN.md explains the design choices.

What this PR adds

30 Lean files (about 11,000 lines) and their 30 imports in AlgoLib.lean. There is no new dependency: the code uses Mathlib and cslib's TimeM, which AlgoLib already requires.

Thesis repository	AlgoLib
ARA/Infrastructure/ (the framework)	AlgoLib/Theory/Randomized/
ARA/Helpers/MultiGraph.lean	AlgoLib/Theory/Graph/MultiGraph.lean
ARA/Helpers/ (Partition, Counting, HarmonicSums)	AlgoLib/Util/
ARA/Algorithms/Karger/Karger.lean	AlgoLib/Algorithms/Graph/MinCut/Karger.lean
the eight other algorithms, and Tutorial.lean	AlgoLib/Algorithms/Randomized/
ARA/FutureWork/SPMF.lean	AlgoLib/Theory/Randomized/FutureWork/SPMF.lean

The entry point is AlgoLib/Algorithms/Randomized/Tutorial.lean. It builds small algorithms step by step and names the file where each tool is defined.

Design in brief

An algorithm is written once, polymorphic in its monad:

{M} [Monad M] [RandMonad M] [MonadCost ℕ M]

RandMonad has one primitive, the uniform draw randFin n. MonadCost has one primitive, tick, which by default does nothing. Proofs use LawfulRandMonad, whose toPMF : M α → PMF α is a monad morphism. So a theorem proved once holds in every lawful monad. PMF and TimeMT ℕ PMF are lawful; IO is not, by design.

The same definition has four readings:

M	Reading
IO	run it
PMF	its output distribution
TimeMT ℕ IO	a benchmark that counts ticks
TimeMT ℕ PMF	the joint distribution of output and cost

TimeMT is a writer-style monad transformer over cslib's TimeM. Expected costs are computed in the last reading.

Correctness comes in three tiers. Dirac: the output distribution is a point mass at a specification. Exact distribution: the output distribution itself is the theorem. Support and probability: every possible output satisfies a property, and the right answer has a probability bound. One-sided error is stated this way. Cost comes in three readings, from strongest to weakest: the cost distribution, the expected cost, and a tail bound by Markov's inequality.

Main results

Here n is the input length, or the number of vertices for Karger, and m the number of edges. Costs are expected numbers of ticks unless stated otherwise.

Algorithm	Correctness	Cost
Karger	Every possible output partitions the vertices into sides, each a cut of the reported value, and that value is at least the minimum cut (karger_isCut). With probability at least 2/(n(n−1)), each side is a minimum cut (karger_finds_min). Running it k times and keeping the smallest reported value gives the minimum value with probability at least 1 − (1 − 2/(n(n−1)))^k (karger_amplified).	≤ (n−2)·m (karger_cost_le). k+1 runs: ≤ (k+1)·(n−2)·m (karger_amplified_cost_le).
Quicksort	The output distribution is a point mass at the sorted list (quicksort_correct).	= 2(n+1)H(n) − 4n on distinct inputs (quicksort_cost_exact). ≤ C(n,2) on all inputs (quicksort_cost_le). Tail: ℙ[cost > k] ≤ C(n,2)/(k+1) (quicksort_runtime_tail).
Quickselect	The output distribution is a point mass at the k-th order statistic (quickselect_correct).	Exact bivariate-harmonic formula on distinct inputs (quickselect_cost_exact). ≤ 4n on distinct inputs (quickselect_cost_le_linear).
Reservoir sampling	ℙ[output = some a] = count(a)/n (reservoir_correct).	= n − 1 (reservoir_cost_exact).
Fisher–Yates	Uniform over the permutations of a list without duplicates (shuffle_uniform).	No tick: it is a sampler.
Schwartz–Zippel	P = 0 gives true with probability 1 (schwartzZippel_complete). Over an integral domain, P ≠ 0 gives true with probability ≤ P.totalDegree / S.card (schwartzZippel_sound).	= 1 (schwartzZippel_cost_exact).
Freivalds	A * B = C gives true with probability 1 (freivalds_complete). A * B ≠ C gives true with probability ≤ 1/2 (freivalds_sound).	= 3n² (freivalds_cost_exact).
Coupon collector	—	Expected number of draws = Σ_{r<n} n/(r+1), that is n·H(n) (couponCollector_cost_exact).
Treap	Every possible output is a binary search tree whose in-order traversal is a permutation of the input (treap_correct).	Expected height ≤ 3·log₂(n+3) + 4 on distinct keys (treap_expected_height_le).

Changes from the thesis code

The namespace ARA became AlgoLib. Imports and the source paths quoted in docstrings follow the new layout, and LawfulRandMonad.lean became Randomness/RandMonad.lean.

Five docstring passages spoke of ARA or of GraphLib, and were rewritten for AlgoLib. The largest is in Theory/Graph/MultiGraph.lean: its section "Standing in for GraphLib" is now "Relation to AlgoLib.Graph".

AlgoLib is on Lean v4.30.0-rc2, the thesis code on v4.32.0. That took three lines:

• Theory/Randomized/Complexity/TimeMT.lean:21 and Theory/Randomized/Tactics.lean:25 declare universe u v w and universe u. The thesis code let autoImplicit bind them, and AlgoLib turns it off.
• Theory/Graph/MultiGraph.lean:8 imports Mathlib.Data.Nat.Lattice. Mathlib renamed that file Mathlib.Order.Lattice.Nat in June 2026.

No theorem statement changed.

Checks

• lake build succeeds. There is no sorry.
• #print axioms on all 340 public theorems and lemmas: each uses at most propext, Classical.choice and Quot.sound.
• The new files raise 52 style-linter warnings and no error. 28 of them flag show used to change the goal.

For the refactor

• 414 declarations sit directly in AlgoLib, for example prob, expVal, Fresh and randIdx. They probably belong in sub-namespaces.
• TimeMT is declared in cslib's namespace Cslib.Algorithms.Lean, next to TimeM. It is a structure. Whether it should be a def like Mathlib's WriterT, so that TimeMT T Id reduces to TimeM T, is the TimeT question still open between us.
• The cost layer (MonadCost, TimeMT) is independent of the RAM model on experimental-RAM-model. How the two should relate is open.
• Tactics.lean adds 30 global simp and grind attributes, almost all on Mathlib's PMF lemmas. No other AlgoLib file uses PMF today, but every file that imports the framework inherits them.
• MultiGraph does not build on AlgoLib.Graph. Karger draws an edge uniformly at random, in a program, and counts crossing edges with multiplicity. So edges are a List (Sym2 α). The module docstring explains the choice and sketches two adapters.
• Some general lemmas, on lists, harmonic sums and PMF, may belong in AlgoLib/Mathlib/, as CONTRIBUTING.md asks. I have not sorted them yet.
• Karger is in Algorithms/Graph/MinCut/, the other algorithms in Algorithms/Randomized/.
• Karger.lean is tidied up to line 579 and Tutorial.lean is reviewed up to line 1307. Markers in the files show where.
• FutureWork/SPMF.lean is unfinished. It proves that retrying until success ends with probability 1 (mass_retry_eq_one), but it is not yet connected to the correctness and cost machinery.