## [Code Comparison]: Lean 4 Proof Strategies for a System of Linear Equations ### Overview The image displays a side-by-side comparison of three Lean 4 code blocks, each attempting to formally prove the same mathematical theorem. The theorem solves a system of two linear equations in variables `f` and `z` over the complex numbers (`ℂ`). The comparison highlights differences in proof strategy, verbosity, and the use of automation tactics between a baseline "LLM" approach and an enhanced "LLM + APOLLO" approach. ### Components/Axes The image is divided into three vertical columns: 1. **Left Column (Header: "LLM" in a red box):** Contains a concise proof attempt. Some lines are highlighted with a pink background. 2. **Middle Column (Header: "LLM + APOLLO" in a green box):** Contains a much more verbose and detailed proof attempt. 3. **Right Column (No header, green background):** Contains a third, distinct proof attempt, also detailed. It appears to be a continuation or alternative to the middle column's proof. **Common Code Structure (All Columns):** * **Imports:** `import Mathlib`, `import Aesop` * **Options:** `set_option maxHeartbeats 0`, `set_option pp.numericTypes true`, `set_option pp.coercions.types true` * **Open Sections:** `open BigOperators Real Nat Topology Rat` * **Theorem Statement:** All three prove a theorem with the same core statement (solving for `f` and `z` given two equations), but with different internal names. ### Detailed Analysis #### **1. Left Column: "LLM" Proof** * **Theorem Name:** `algebra_2varlineareq_fp3zeq11_3tfm1m5zeqn68_feqn10_zeq7_llm` * **Hypotheses:** * `h0 : f + (3 : ℂ) * z = (11 : ℂ)` * `h1 : (3 : ℂ) * (f - 1) - (5 : ℂ) * z = (-68 : ℂ)` * **Goal:** `f = (-10 : ℂ) ∧ z = (7 : ℂ)` * **Proof Strategy:** A short, direct proof using the `linarith` (linear arithmetic) tactic. 1. Simplifies the second equation (`h1`) using `mul_sub` to get `h2 : 3 * f - 3 - 5 * z = -68`. 2. Combines like terms to isolate `3*f - 5*z`, creating `h3 : 3 * f - 5 * z = -65`. **This line is highlighted in pink.** 3. Uses `linarith [h0, h3]` to solve for `z`, creating `z_eq : z = 7`. **This line is highlighted in pink.** 4. Uses `linarith [h0, z_eq]` to solve for `f`, creating `f_eq : f = -10`. **This line is highlighted in pink.** 5. Concludes with `exact And.intro f_eq z_eq`. * **Observation:** The proof is compact but relies heavily on the `linarith` tactic to perform multiple algebraic steps implicitly. The pink highlights may indicate steps where the proof is less transparent or where a more advanced prover (like APOLLO) intervened. #### **2. Middle Column: "LLM + APOLLO" Proof** * **Theorem Name:** `algebra_2varlineareq_fp3zeq11_3tfm1m5zeqn68_feqn10_zeq7_apollo` * **Hypotheses:** Identical to the left column (`h0`, `h1`). * **Goal:** Identical to the left column. * **Proof Strategy:** An extremely verbose, step-by-step proof that explicitly performs each algebraic manipulation. It uses a wide array of tactics (`norm_num`, `simp_all`, `ring_nf`, `native_decide`, `linarith`, `nlinarith`) in a trial-and-error fashion at many steps. * **Key Steps:** * Creates `h2` and `h3` similar to the LLM proof but with explicit tactic sequences. * Expands and manipulates equations to isolate terms (e.g., `h_expanded`, `h_added`, `h_add`, `h_sum`, `h_subst`, `h_simpl`). * Solves for `z` (`z_eq`) and `f` (`f_eq_def`, `f_eq`) through explicit substitution and simplification, culminating in `have isolate_z : (14 : ℂ) * z = 98`. * The proof in this column is cut off at the bottom with an ellipsis (`...`), indicating it continues. #### **3. Right Column: Alternative Detailed Proof** * **Theorem Name:** Not fully visible, but the code is a continuation of a proof. * **Proof Strategy:** This column shows a different detailed proof path, focusing on manipulating equations to isolate `z`. * **Key Steps:** * Defines intermediate equalities `eq3`, `eq4`, and `eq_final`. * Solves for `z` using `have z_sol : z = (7 : ℂ) := by norm_num`. * Explicitly handles the non-zero denominator: `have h_nonzero : (14 : ℂ) ≠ 0 := by norm_num`. * Uses the inverse to solve: `have z_inv : z = 98 * ((14 : ℂ)⁻¹) := by exact (eq_mul_inv_iff_mul_eq₀ h_nonzero).mpr isolate_z`. * Simplifies the division: `have z_simpl : 98 / (14 : ℂ) = (7 : ℂ) := by norm_num`. * Solves for `f` (`f_eq`) using the first hypothesis `h0`. * Concludes with `exact And.intro f_eq z_eq`. ### Key Observations 1. **Proof Length & Transparency:** The "LLM" proof is short and opaque, relying on `linarith` as a black box. The "LLM + APOLLO" proofs are orders of magnitude longer, making every algebraic step explicit. 2. **Tactic Usage:** The enhanced proofs employ a much broader and more repetitive set of tactics, suggesting a search-based or guided proof strategy. 3. **Common Goal:** All three proofs successfully establish the same theorem: `f = -10` and `z = 7`. 4. **Visual Coding:** The red "LLM" header and pink highlights contrast with the green "LLM + APOLLO" header and green background, visually framing the comparison as between a baseline and an improved method. ### Interpretation This image is a technical comparison of automated theorem proving strategies in the Lean 4 proof assistant. It demonstrates the difference between a proof generated by a standard Large Language Model (LLM) and one enhanced by a system called APOLLO. * **What it shows:** The LLM produces a correct but minimally explanatory proof. It gets the right answer but doesn't "show its work" in a human-readable way. The APOLLO-enhanced proofs, while verbose to the point of being impractical for a human to write, decompose the problem into a long chain of simple, verifiable steps. This makes the proof's logic completely transparent and robust. * **Why it matters:** In formal verification, the goal is not just correctness but also trust and understandability. The verbose proofs act as a "certificate" where each step can be independently checked by simple tactics (`norm_num`). This approach is less elegant but potentially more reliable and easier to debug. The comparison likely aims to showcase APOLLO's ability to generate more detailed, trustworthy, and human-auditable formal proofs compared to a vanilla LLM. * **Underlying Pattern:** The core mathematical task is solving the linear system: 1. `f + 3z = 11` 2. `3(f - 1) - 5z = -68` → `3f - 3 - 5z = -68` → `3f - 5z = -65` Subtracting 3 times the first equation from the second: `(3f - 5z) - 3*(f + 3z) = -65 - 3*11` → `-14z = -98` → `z = 7`. Substituting back gives `f = -10`. The APOLLO proofs essentially mechanize this manual algebraic process in excruciating detail.