Latest Articles

Working with Existential Quantifiers, Universal Quantifiers, and Classical Reasoning in Lean

November 27, 2025 • By Sham Prop Lean4

A comprehensive collection of Lean 4 examples covering existential and universal quantifiers, and the interplay between constructive and classical reasoning.

Existential Quantifier

November 25, 2025 • By Sham lean4 proof

A look at proving existential statements in Lean 4 with calculation blocks.

Distributive Law of Propositional Logic in Lean

November 25, 2025 • By Sham lean4 proof

example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := by sorry

Archive — Other Notes

The following are shorter notes and scanned posts added to the site. They are linked here and kept as individual pages in posts/.

The Bow - Tie Space — March 30, 2023
Completion of Polynomial Space and Stone-Weierstrass — May 30, 2020
Arzelà–Ascoli theorem — July 11, 2019
p‑Groups — July 11, 2019
Cauchy's Theorem (McKay proof) — July 10, 2019
Elements in orbit is the index of stabilizer — July 10, 2019
1985 B5 (Putnam) — July 09, 2019
C[0,1] is not complete with L^1 metric — July 09, 2019
Finite subgroups of GL(n,Z) are finite — July 08, 2019
Algebraic Closure of a field — April 12, 2018