## Screenshot: Lean/Coq Code Comparison (LLM vs. LLM + APOLLO) ### Overview The image shows two side-by-side code snippets written in a formal proof assistant (likely Lean or Coq), comparing implementations of a mathematical theorem (`mathd_algebra_141`) using different proof strategies. The left snippet is labeled "LLM", and the right is labeled "LLM + APOLLO". Both snippets define a theorem about real numbers `a` and `b` with the constraint `a * b = 180`, and compute `a² + b²` using algebraic manipulations. --- ### Components/Axes - **Imports**: - `import Mathlib` - `import Aesop` - **Options**: - `set_option maxHeartbeats 0` (disables interactive proof search) - **Open Statements**: - Left: `open BigOperators Real Nat Topology Rat` - Right: `open BigOperators Real Nat Topology Rat` (identical to left) - **Theorem Declaration**: - `theorem mathd_algebra_141_llm (a b : ℝ) (h1 : a * b = 180) ...` - `theorem mathd_algebra_141_apollo (a b : ℝ) (h1 : a * b = 180) ...` - **Key Variables**: - `h1 : a * b = 180` - `h2 : 2 * (a + b) = 54` (derived from `a + b = 27`) - `h3 : a + b = 27` - `h4 : (a + b)² = 729` --- ### Detailed Analysis #### Left Snippet (LLM) 1. **Proof Steps**: - `have h3 : a + b = 27 := by field_simp [h2]` - Uses `field_simp` to derive `a + b = 27` from `2*(a + b) = 54`. - `have h4 : (a + b)² = 729 := by rw [h3]` - Rewrites `(a + b)²` using `h3`. - `have expand : a² + b² = (a + b)² - 2*a*b := by ring` - Applies ring theory to expand `(a + b)²`. - `have step1 : a² + b² = 729 - 2*a*b := by rw [expand, h4]` - Substitutes `h4` into the expanded form. - `have step2 : 729 - 2*a*b = 729 - 360 := by rw [h1]` - Replaces `a*b` with `180` using `h1`. - `have step3 : 729 - 360 = 369 := by norm_num` - Computes the final value. - `exact step1.trans (step2.trans step3)` - Chains equalities using transitivity. 2. **Annotations**: - `#1`, `#2`, `#3` in red (likely indicating proof steps or priorities). #### Right Snippet (LLM + APOLLO) 1. **Proof Steps**: - `have h3 : a + b = 27 := by linarith` - Uses `linarith` (linear arithmetic) to derive `a + b = 27` directly. - `have expand : a² + b² = (a + b)² - 2*a*b := by ring` - Same as left snippet. - `have step1 : a² + b² = 729 - 2*a*b := by rw [expand, h4]` - Same as left snippet. - `have step2 : 729 - 2*a*b = 729 - 360 := by linarith` - Uses `linarith` instead of `rw [h1]` for simplification. - `have step3 : 729 - 360 = 369 := by norm_num` - Same as left snippet. - `linarith` - Final step uses `linarith` to automate the entire proof. 2. **Annotations**: - `#1`, `#2`, `#3` in green (consistent with LLM + APOLLO). --- ### Key Observations 1. **Tactics Differences**: - LLM uses manual rewriting (`rw`) and transitivity (`trans`), while LLM + APOLLO leverages `linarith` for automated simplification. - APOLLO reduces the number of explicit steps (e.g., `linarith` replaces `rw [h1]` and intermediate steps). 2. **Code Structure**: - Both snippets share identical imports, options, and variable declarations. - The right snippet (APOLLO) is more concise, relying on automated tactics. 3. **Annotations**: - Red annotations (`#1`, `#2`, `#3`) on the left suggest manual step prioritization. - Green annotations on the right indicate APOLLO’s streamlined approach. --- ### Interpretation The comparison highlights the impact of APOLLO on proof automation: - **Efficiency**: APOLLO reduces manual steps by integrating linear arithmetic (`linarith`), which automatically handles equality chains and simplifications. - **Readability**: The LLM snippet requires explicit rewriting and transitivity, while APOLLO abstracts these steps. - **Correctness**: Both snippets arrive at the same result (`a² + b² = 369`), confirming the theorem’s validity. The use of `linarith` in APOLLO demonstrates how automated tactics can simplify proofs in formal verification, reducing human error and effort. The red/green annotations visually emphasize the contrast between manual and automated approaches.