## 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.