Lean 4 Proof Portfolio

Design Philosophy

Automation is deliberately limited to maintain transparency in proof structure — tactics like simp, omega, and linarith are avoided in favor of explicit lemma invocation. This constraint demonstrates understanding of underlying proof mechanics rather than tactical pattern matching. Complex theorems are decomposed into manageable subgoals using helper lemmas and have blocks, mirroring mathematical practice of building layered arguments.

Formalization Files

• Basic.lean — Associativity, distributivity. Establishes induction patterns and rewriting discipline.
• Arithmetic.lean — Cancellation for addition, monotonicity of multiplication. Converts between inductive and existential representations of ordering.
• NumberTheory.lean — Divisibility closure under addition and the parity dichotomy. Explicit witness construction and case analysis.
• OrderAndInequalities.lean — Order preservation under addition, cancellation for strict inequality. Proof by contradiction combined with order reflection.
• Combinatorics.lean — Closed-form triangular number sum via finset operations. Handles truncating division in ℕ through even/odd case analysis.
• Advanced.lean — Uniqueness of quotient and remainder in the division algorithm. Capstone result coordinating arithmetic, order theory, and propositional logic.

Selected Highlights

Division algorithm uniqueness (div_mod_unique): Given two representations of a natural number as quotient-remainder pairs with bounded remainders, both must be identical. The proof establishes quotient equality via contradiction and case analysis on ordering, then derives remainder equality through direct cancellation.

Multiplication preserves inequality (my_mul_le_mul_left): Proved by converting the inductive ordering relation to its existential representation, constructing an appropriate witness, and reconstructing the target inequality — illustrating work across different formulations of the same concept.