\n ## System Architecture Diagram: Automated Theorem Proving with Premise Retrieval ### Overview The image is a technical system architecture diagram illustrating an automated reasoning or proof-generation system. It depicts the flow of information between a proof state, a mathematical library, a premise retrieval mechanism, and a tactic generator, culminating in the generation of a Lean 4 code tactic. The diagram is divided into three main vertical sections: a **Proof Tree** on the left, a **System Flow** in the center, and a **Code Output** on the right. ### Components/Axes The diagram is composed of the following labeled components and their spatial relationships: 1. **Left Section: Proof Tree & State** * **Top Box (State):** Labeled `State`. Contains a proof state represented as `(S : Type u₁) (inst : Mul S)` and two hypotheses: * `h₁ : ∀ (a b : S), a * b = a` * `h₂ : ∀ (a b : S), a * b = b * a` * **Middle Box (Tactic):** Labeled `Tactic`. Shows the application of a rewrite tactic: `rw [Cardinal.le_one_iff_subsingleton]`. * **Bottom Box (Resulting State):** The result of applying the tactic. It contains the same `(S : Type u₁) (inst : Mul S)` and hypotheses `h₁` and `h₂`, but the goal has changed to `Cardinal.mk S ≤ 1 ↔ Subsingleton S`. * **Arrows:** A solid arrow labeled `Tactic` points from the top State box to the middle Tactic box. Another solid arrow points from the Tactic box to the bottom Resulting State box. Dashed arrows point downward from the bottom box, indicating further proof steps. 2. **Center Section: System Flow** * **Math Library Icon:** A classical building icon labeled `math library`. * **Premise Retriever:** A dashed box labeled `Premise Retriever`. It receives input from the `State` (via a dashed arrow) and the `math library` (via a solid arrow). Inside, it lists `Retrieved Premises`: * `theorem Cardinal.le_one_iff_subsingleton` * `theorem Cardinal.mk_eq_one` * `theorem Cardinal.eq_one_iff_unique` * **Tactic Generator:** A dashed box labeled `Tactic Generator`. It receives the retrieved premises (via a dashed arrow from the Premise Retriever) and outputs a tactic (via a solid arrow labeled `rw [Cardinal.le_one_iff_subsingleton]`) which feeds into the `Tactic` box in the Proof Tree. 3. **Right Section: Code Output** * A block of code written in the **Lean 4** programming language (a functional programming language used for formal verification). The code is presented in a monospaced font on a light background. ### Detailed Analysis **Proof Tree Transcription:** * **Initial State:** `(S : Type u₁) (inst : Mul S)` with hypotheses `h₁ : ∀ (a b : S), a * b = a` and `h₂ : ∀ (a b : S), a * b = b * a`. * **Applied Tactic:** `rw [Cardinal.le_one_iff_subsingleton]` * **Resulting State:** `(S : Type u₁) (inst : Mul S)` with the same hypotheses, but the goal is now `Cardinal.mk S ≤ 1 ↔ Subsingleton S`. **System Flow Details:** The diagram shows a closed-loop process: 1. The current proof `State` is sent to the `Premise Retriever`. 2. The `Premise Retriever` queries the `math library` (likely Mathlib for Lean) and retrieves relevant theorem statements (`Cardinal.le_one_iff_subsingleton`, `Cardinal.mk_eq_one`, `Cardinal.eq_one_iff_unique`). 3. These retrieved premises are passed to the `Tactic Generator`. 4. The `Tactic Generator` selects and formats a tactic (`rw [Cardinal.le_one_iff_subsingleton]`). 5. This tactic is applied to the original `State`, transforming it into the new `Resulting State`. **Lean 4 Code Transcription:** ```lean import Mathlib variable {S : Type*} [Mul S] example (h₁ : ∀ (a b : S), a * b = a) (h₂ : ∀ (a b : S), a * b = b * a) : Cardinal.mk S ≤ 1 := by rw [Cardinal.le_one_iff_subsingleton] refine ⟨?_⟩ intro a b rw [← h₁ a b] rw [h₂ a b] exact h₁ b a ``` * **Language:** Lean 4. * **Content:** The code defines a theorem `example` stating that under hypotheses `h₁` and `h₂` (which describe a commutative monoid where every product equals both its left and right arguments), the cardinality of the type `S` is at most 1. The proof script uses the `rw` tactic with the same theorem retrieved by the system (`Cardinal.le_one_iff_subsingleton`), followed by a `refine` tactic to handle the resulting goal, and concludes with basic rewrites and an exact proof term. ### Key Observations 1. **Specific Theorem Focus:** The entire process shown is centered on the theorem `Cardinal.le_one_iff_subsingleton`. The Premise Retriever finds it, the Tactic Generator uses it, and the Proof Tree applies it. 2. **Hypothesis-Driven Proof:** The initial state's hypotheses (`h₁`, `h₂`) are very strong, implying the structure `S` is trivial (all elements are equal). The retrieved theorem and the final Lean code connect this triviality to the cardinality being ≤ 1. 3. **Diagram vs. Code Discrepancy:** The diagram's `Resulting State` shows the goal as `Cardinal.mk S ≤ 1 ↔ Subsingleton S`, which is the *full* statement of the retrieved theorem. However, the Lean code on the right shows the tactic `rw [Cardinal.le_one_iff_subsingleton]` being applied to a goal of `Cardinal.mk S ≤ 1`. This suggests the diagram illustrates the *internal* state transformation (applying the biconditional), while the code shows the *user-facing* proof step where the biconditional is used to simplify the goal. 4. **Spatial Flow:** The legend (`Retrieved Premises`) is centrally located within the `Premise Retriever` box. The flow arrows clearly show data moving from left (proof state) to center (retrieval/generation) and back to left (application), with the final code output on the far right. ### Interpretation This diagram illustrates a **neuro-symbolic or retrieval-augmented approach to automated theorem proving**. It demonstrates a system that does not generate proof tactics from scratch but instead: 1. **Analyzes** the current proof state (goals and hypotheses). 2. **Retrieves** relevant lemmas from a vast formal library (Mathlib) based on that analysis. 3. **Selects** an appropriate tactic (a rewrite using a specific theorem) to make progress. 4. **Applies** it to transform the proof state. The specific example is pedagogical: it shows how the system can recognize that the hypotheses `h₁` and `h₂` imply the type `S` has at most one element (it's a "subsingleton") and retrieves the exact theorem (`Cardinal.le_one_iff_subsingleton`) that formally links this property to cardinality. The Lean code on the right is the concrete output of this process—a human-readable proof script that a user could execute. The system's value lies in bridging the gap between the vast knowledge contained in formal libraries (like Mathlib) and the tactical proof search process, effectively giving the prover a "memory" and a way to leverage existing mathematical results. The diagram emphasizes the *retrieval* step as a core component of intelligent proof automation.