## Mathematical Formalization Code Snippets: Project Examples ### Overview The image displays five distinct code blocks, each representing a formal mathematical statement (lemma or theorem) and its proof, written in the Lean 4 proof assistant language. These snippets are sourced from different formalization projects or libraries, as indicated by their titles. The code is presented in a monospaced font with syntax highlighting (keywords in blue, definitions/tactics in green, types in brown). The layout is asymmetrical, with three blocks on the left and two on the right. ### Components/Axes The image is organized into labeled sections, each containing a code block within a rounded rectangle. The labels are: * **PFR** (Top-Left) * **SciLean** (Middle-Left) * **Coxeter** (Bottom-Left) * **MiniF2F** (Top-Right) * **Formal Book** (Bottom-Right) There are no traditional chart axes, legends, or data points. The "data" consists of the textual code itself. ### Detailed Analysis / Content Details #### **PFR (Top-Left)** * **Label:** `PFR` * **Code Transcription:** ```lean lemma condRho_of_translate {Ω S : Type*} [MeasureSpace Ω] (X : Ω → G) (Y : Ω → S) (A : Finset G) (s:G) : condRho (fun ω ↦ X ω + s) Y A = condRho X Y A := by simp only [condRho, rho_of_translate] ``` * **Content:** This is a lemma about a conditional expectation operator (`condRho`) in the context of measure theory. It states that translating the random variable `X` by a constant `s` does not change the value of `condRho`. The proof is completed by simplification (`simp`) using the definitions of `condRho` and `rho_of_translate`. #### **SciLean (Middle-Left)** * **Label:** `SciLean` * **Code Transcription:** ```lean theorem re_float (a : Float) : RCLike.re a = a := by exact RCLike.re_eq_self_of_le le_rfl ``` * **Content:** This theorem asserts that for a floating-point number `a` (treated as an element of a complex-like ring `RCLike`), its real part (`RCLike.re`) is equal to itself. The proof uses an exact application of a lemma `RCLike.re_eq_self_of_le` with a reflexivity proof (`le_rfl`). #### **Coxeter (Bottom-Left)** * **Label:** `Coxeter` * **Code Transcription:** ```lean lemma invmap.of_eq {S:Set G} [CoxeterSystem G S] {s :S} : invmap S s = s := by simp [CoxeterSystem.Presentation.invmap] unfold CoxeterSystem.toMatrix apply CoxeterSystem.monoidLift.mapLift.of ``` * **Content:** This lemma concerns Coxeter systems. It states that the inverse map (`invmap`) of a generator `s` from the set `S` is equal to `s` itself. The proof proceeds by simplifying the definition of `invmap`, unfolding the `toMatrix` definition, and then applying a property (`of`) from the monoid lift. #### **MiniF2F (Top-Right)** * **Label:** `MiniF2F` * **Code Transcription (Theorem 1):** ```lean theorem induction_12dvd4expnp1p20 (n : ℕ) : 12 | 4^(n+1) + 20 := by norm_num induction' n with n hn simp omega ``` * **Content:** This theorem from the MiniF2F benchmark states that for any natural number `n`, 12 divides `4^(n+1) + 20`. The proof uses numeric normalization (`norm_num`), induction on `n`, simplification (`simp`), and the omega tactic for linear arithmetic. * **Code Transcription (Theorem 2):** ```lean theorem amc12a_2002_p6 (n : ℕ) (h₀ : 0 < n) : ∃ m, (m > n ∧ ∃ p, m * p ≤ m + p) := by lift n to ℕ+ using h₀ cases' n with n exact (_, lt_add_of_pos_right _ zero_lt_one, 1, by simp) ``` * **Content:** This theorem, sourced from the AMC 12A 2002 competition (problem 6), states that for any positive natural number `n`, there exists a natural number `m` greater than `n` such that there exists a `p` where `m * p ≤ m + p`. The proof lifts `n` to a positive natural number, performs case analysis, and provides a witness (`m = n+1`, `p = 1`). #### **Formal Book (Bottom-Right)** * **Label:** `Formal Book` * **Code Transcription:** ```lean theorem wedderburn (h: Fintype R): IsField R := by apply Field.toIsField ``` * **Content:** This theorem states Wedderburn's little theorem: if a finite ring `R` (with a finite type `Fintype R`) is a division ring, then it is a field (`IsField R`). The proof applies the lemma `Field.toIsField`. ### Key Observations 1. **Diversity of Domains:** The snippets cover distinct areas of mathematics: measure theory (PFR), numerical analysis (SciLean), algebra/combinatorics (Coxeter), number theory and competition math (MiniF2F), and ring theory (Formal Book). 2. **Proof Techniques:** A variety of Lean 4 tactics are demonstrated, including `simp`, `exact`, `unfold`, `apply`, `norm_num`, `induction'`, `omega`, and `cases'`. 3. **Syntax Highlighting:** Keywords (`lemma`, `theorem`, `by`, `simp`, `exact`, etc.) are consistently highlighted in blue. Definitions, tactics, and specific constants (`condRho`, `rho_of_translate`, `RCLike.re_eq_self_of_le`, `CoxeterSystem.Presentation.invmap`, `lt_add_of_pos_right`, `Field.toIsField`) are highlighted in green. Type constructors and constants (`Type*`, `MeasureSpace`, `Finset`, `ℕ`, `Float`, `Set`, `CoxeterSystem`, `Fintype`) are in brown. 4. **Layout:** The code blocks are arranged in a non-grid, visually balanced manner. The `MiniF2F` block is the largest, containing two separate theorems. ### Interpretation This image serves as a showcase or catalog of formalized mathematical results from various Lean 4 projects. It is not a data chart but a **technical document snippet**. The primary information is the code itself, which provides concrete examples of: * **Formal Statement:** How mathematical concepts are precisely encoded in a dependently typed language. * **Proof Sketch:** The high-level structure of the machine-checked proof, indicated by the tactic steps. * **Project Scope:** The titles (`PFR`, `SciLean`, etc.) hint at the broader libraries or formalization efforts these snippets belong to, suggesting active work in formalizing diverse mathematical fields. The value lies in the **precision and verifiability** of the content. Each snippet is a self-contained, machine-verifiable claim. For a researcher or developer in formal methods, this image provides quick reference examples of Lean 4 syntax and proof patterns across different domains. The highlighted green text likely draws attention to key definitions or lemmas that are central to each proof's strategy.