Different Proofs

 Different Proofs🔗

Compiled2026-06-18T16:17:11ZProject1f3ce5dBasel problem: Parseval and Cauchy cotangent-squeeze proofs (#19)Leanleanprover/lean4:v4.30.0VersoBlueprintv4.30.0@357468f3df7fMathlibv4.30.0@c5ea00351c28

This blueprint tracks formalizations of multiple proofs of the same theorem. The Lean declarations live in the DifferentProofs library, while this Verso document records the informal statements, proof sketches, and dependency graph.

Contents

  1. 1. Fermat's Little Theorem
  2. 2. Infinitude of Primes
  3. 3. Irrationality of √2
  4. 4. Basel problem
  5. Dependency Graph
  6. Blueprint Summary