## Code Comparison: LLM vs. LLM + APOLLO ### Overview The image presents a side-by-side comparison of code snippets, labeled "LLM" on the left and "LLM + APOLLO" on the right. Both snippets appear to be related to mathematical theorem proving, with similar initializations and a theorem definition. The key difference lies in the handling of cases within the induction proof, where "LLM + APOLLO" introduces an additional induction step. ### Components/Axes * **Headers:** * Left: "LLM" (red background) * Right: "LLM + APOLLO" (green background) * **Code Blocks:** Two code blocks containing mathematical definitions and proofs. * **Annotations:** "#1" and "#2" are used to highlight specific lines in both code blocks. ### Detailed Analysis or ### Content Details **Left Code Block (LLM):** * **Imports:** * `import Mathlib` * `import Aesop` * **Options:** * `set_option maxHeartbeats 0` * **Open:** * `open BigOperators Real Nat Topology Rat` * **Theorem:** * `theorem induction_pord1p1on2powklt5on2_1lm (n k : N)` * `(h₀ : 0 < n) :` * `(Π k in Finset.Icc 1 n, 1 + (1 : R) / 2 ^ k) < 5 / 2 := by` * **Proof:** * `induction n with` * `| zero =>` * `contradiction` * `| succ n hn =>` * `cases n with` * `| zero =>` * `norm_num` `#1` (highlighted in pink) * `| succ n =>` * `simp_all [Finset.prod_Icc_succ_top, Nat.cast_succ, div_eq_mul_inv]` * `norm_num` `#2` (highlighted in pink) * `ring_nf` (highlighted in pink) * `linarith` (highlighted in pink) **Right Code Block (LLM + APOLLO):** * **Imports:** * `import Mathlib` * `import Aesop` * **Options:** * `set_option maxHeartbeats 0` * **Open:** * `open BigOperators Real Nat Topology Rat` * **Theorem:** * `theorem induction_pord1p1on2powklt5on2_apollo (n k : N)` * `(h₀ : 0 < n) :` * `(Π k in Finset.Icc 1 n, 1 + (1 : R) / 2 ^ k) < 5 / 2 := by` * **Proof:** * `induction n with` * `| zero =>` * `contradiction` * `| succ n hn =>` * `cases n with` * `| zero =>` * `norm_num` `#1` (highlighted in light green) * `induction k with` * `| zero =>` * `norm_num` * `[Finset.prod_Icc_succ_top] at hn h₀ <;> linarith` * `| succ k ih =>` * `cases k with` * `| zero =>` * `norm_num` * `[Finset.prod_Icc_succ_top] at hn h₀ <;> linarith` * `| succ k =>` * `simp_all [Finset.prod_Icc_succ_top, pow_succ, mul_comm]` * `linarith` * `| succ n =>` * `simp_all [Finset.prod_Icc_succ_top, Nat.cast_succ, div_eq_mul_inv]` * `norm_num` `#2` (highlighted in light green) * `ring_nf` (highlighted in light green) * `linarith` (highlighted in light green) ### Key Observations * Both code blocks define a theorem named `induction_pord1p1on2powklt5on2_...` with slightly different suffixes (`_1lm` vs `_apollo`). * The initial setup (imports, options, open statements, theorem definition) is identical in both blocks. * The key difference is in the handling of the `cases n with | zero =>` branch within the `induction n with | succ n hn =>` case. The "LLM + APOLLO" version introduces an additional `induction k with` step, providing more granular control over the proof. * Annotations `#1` and `#2` highlight corresponding lines in both code blocks, indicating specific points of interest or comparison. * The highlighting colors (pink for LLM, light green for LLM + APOLLO) visually distinguish the code blocks and their respective annotations. ### Interpretation The image demonstrates a comparison between two approaches to proving a mathematical theorem. The "LLM + APOLLO" version utilizes a more refined induction strategy, potentially leading to a more robust or efficient proof. The additional `induction k with` step in the "LLM + APOLLO" version suggests a more detailed analysis of the base case within the inductive step. The annotations highlight the specific lines where the proof strategies diverge, allowing for a focused comparison of the two approaches. The use of different highlighting colors enhances the visual clarity of the comparison.

## Code Comparison Diagram: LLM vs. LLM + APOLLO Lean 4 Proofs ### Overview The image presents a side-by-side comparison of two code snippets written in the Lean 4 theorem proving language. The left panel displays code generated by a baseline "LLM" (Large Language Model), while the right panel displays code generated by an augmented system labeled "LLM + APOLLO". The diagram highlights specific differences in the proof tactics used by each system, using color-coded blocks and numbered tags to draw attention to areas where APOLLO modifies, expands, or deletes the baseline LLM's output. ### Components and Spatial Grounding The image is divided into two distinct vertical panels: * **Left Panel (LLM):** Enclosed in a red border with a red header box at the top center containing the text "LLM" in black. The background is a very faint red/pink. It contains Lean 4 code. Two specific areas are highlighted with a solid light red background and tagged with "#1" and "#2" on their right edges. * **Right Panel (LLM + APOLLO):** Enclosed in a green border with a green header box at the top center containing the text "LLM + APOLLO" in black. The background is a very faint green. It contains Lean 4 code. Two specific areas are highlighted with a solid light green background and tagged with "#1" and "#2" on their right edges. Text within the "#2" highlight features a strikethrough effect. ### Content Details: Transcription and Component Isolation #### 1. Left Panel: LLM This panel shows the baseline proof attempt. **Transcription:** ```lean import Mathlib import Aesop set_option maxHeartbeats 0 open BigOperators Real Nat Topology Rat theorem induction_pord1p1on2powklt5on2_llm (n k : ℕ) (h₀ : 0 < n) : (∏ k in Finset.Icc 1 n, 1 + (1 : ℝ) / 2 ^ k) < 5 / 2 := by induction n with | zero => contradiction | succ n hn => cases n with | zero => norm_num #1 | succ n => simp_all [Finset.prod_Icc_succ_top, Nat.cast_succ, div_eq_mul_inv] norm_num #2 ring_nf linarith ``` *Spatial Notes for Left Panel:* * **Highlight #1:** The line `norm_num` under the `| zero =>` case has a red background. The tag `#1` is placed immediately to the right of `norm_num`. * **Highlight #2:** The block of three lines (`norm_num`, `ring_nf`, `linarith`) at the very end of the code has a red background. The tag `#2` is placed immediately to the right of the `norm_num` line within this block. #### 2. Right Panel: LLM + APOLLO This panel shows the modified proof attempt. The setup and initial theorem declaration are identical, except for the theorem name suffix (`_apollo` instead of `_llm`) and slight differences in line wrapping. **Transcription:** ```lean import Mathlib import Aesop set_option maxHeartbeats 0 open BigOperators Real Nat Topology Rat theorem induction_pord1p1on2powklt5on2_apollo (n k : ℕ) (h₀ : 0 < n) : (∏ k in Finset.Icc 1 n, 1 + (1 : ℝ) / 2 ^ k) < 5 / 2 := by induction n with | zero => contradiction | succ n hn => cases n with | zero => norm_num induction k with | zero => norm_num [Finset.prod_Icc_succ_top] at hn h₀ <;> linarith | succ k ih => cases k with | zero => norm_num [Finset.prod_Icc_succ_top] at hn h₀ <;> linarith | succ k => simp_all [Finset.prod_Icc_succ_top, pow_succ, mul_comm] linarith #1 | succ n => simp_all [Finset.prod_Icc_succ_top, Nat.cast_succ, div_eq_mul_inv] ~~norm_num~~ #2 ~~ring_nf~~ ~~linarith~~ ``` *Spatial Notes for Right Panel:* * **Highlight #1:** A large green background block begins at the `norm_num` line under the `| zero =>` case and extends down to the `linarith` line just before `| succ n =>`. The tag `#1` is placed to the far right, aligned with the top line (`norm_num`) of this highlighted block. * **Highlight #2:** A green background block covers the final three lines of the code. The text of these three lines (`norm_num`, `ring_nf`, `linarith`) is crossed out with a strikethrough line. The tag `#2` is placed immediately to the right of the crossed-out `norm_num`. ### Key Observations 1. **Expansion at #1:** The baseline LLM attempts to solve the `| zero =>` case of the `cases n` block with a single `norm_num` tactic. This is highlighted in red, implying it fails or is insufficient. The APOLLO system expands this single line into a complex, 14-line nested induction on `k` (`induction k with...`), handling multiple sub-cases to properly close the goal. 2. **Deletion at #2:** At the end of the proof, under the `| succ n =>` case, the baseline LLM generates three tactics: `norm_num`, `ring_nf`, and `linarith` after a `simp_all` call. The APOLLO system highlights these exact three lines and applies a strikethrough, indicating that these tactics are either unnecessary (the proof is already closed by `simp_all`), redundant, or cause an error in the Lean environment. ### Interpretation This image serves as a technical demonstration of the "APOLLO" system's capabilities in the domain of formal theorem proving (specifically using Lean 4). It illustrates that while a standard LLM can generate the broad structure of a mathematical proof, it often fails at specific logical junctions by either hallucinating overly simplistic tactics that don't work (Observation #1) or by appending unnecessary/failing steps at the end of a branch (Observation #2). The APOLLO system appears to act as an agentic or iterative wrapper around the LLM. By comparing the two panels, we can deduce APOLLO's function: * **Generative Repair:** When a tactic fails (like the first `norm_num`), APOLLO does not just give up; it generates a deeper, structurally sound sub-proof (the nested induction on `k`) to bridge the logical gap. * **Pruning:** APOLLO recognizes when the goal state has been achieved or when subsequent tactics are invalid, actively removing them (the struck-through text) to ensure the final proof script compiles cleanly without errors. Ultimately, the data suggests that combining an LLM with the APOLLO framework transforms an incomplete or broken formal proof into a verified, working proof by dynamically expanding necessary logic and pruning faulty logic.

\n ## Code Snippets: LLM vs. LLM + APOLLO ### Overview The image presents two code snippets, likely from a formal verification or theorem proving environment (Lean 4). The snippets appear to define a theorem named `induction_pordipion2powklt5on2_llm` and `induction_pordipion2powklt5on2_apollo` respectively. The code uses mathematical notation and logical operators. The snippets are visually similar, but the right-hand side (labeled "LLM + APOLLO") contains additional lines of code compared to the left-hand side ("LLM"). ### Components/Axes There are no axes or traditional chart components. The image consists of two blocks of text representing code. Each block has a header indicating "LLM" or "LLM + APOLLO". The code is structured with indentation to represent the logical hierarchy. ### Detailed Analysis or Content Details **Left Snippet (LLM):** ``` import Mathlib import Aesop set_option maxHeartbeats 0 open BigOperators Real Nat Topology Rat theorem induction_pordipion2powklt5on2_llm (n : N) (h₀ : 0 < n) : (∀ k in Finset.Icc 1, n + (1 : ℛ) ^ 2 ^ k) < 5 / 2 := by induction n with | zero => contradiction | succ n hh => cases n with | zero => norm_num #1 | succ n => simp all [Finset.prod_Icc succ top, Nat.cast_succ, div_eq_mul_inv] norm_num #2 ring_nf linarith ``` * **Imports:** `Mathlib`, `Aesop` * **Option:** `set_option maxHeartbeats 0` * **Open Namespace:** `BigOperators Real Nat Topology Rat` * **Theorem Name:** `induction_pordipion2powklt5on2_llm` * **Input:** `n : N` (n is a natural number), `h₀ : 0 < n` (n is greater than 0) * **Statement:** `(∀ k in Finset.Icc 1, n + (1 : ℛ) ^ 2 ^ k) < 5 / 2` (For all k in the closed interval from 1 to n, n plus 1 raised to the power of 2 to the power of k is less than 5/2) * **Proof:** `by induction n with ...` (Proof by induction on n) * **Base Case:** `zero => contradiction` (If n is zero, a contradiction arises) * **Inductive Step:** `succ n hh => cases n with ...` (If n is a successor, consider two cases) * **Case 1:** `zero => norm_num #1` (If n is zero, apply `norm_num #1`) * **Case 2:** `succ n => simp all [Finset.prod_Icc succ top, Nat.cast_succ, div_eq_mul_inv] norm_num #2 ring_nf linarith` (If n is a successor, apply simplification rules, `norm_num #2`, ring normalization, and linear arithmetic) **Right Snippet (LLM + APOLLO):** ``` import Mathlib import Aesop set_option maxHeartbeats 0 open BigOperators Real Nat Topology Rat theorem induction_pordipion2powklt5on2_apollo (n : N) (h₀ : 0 < n) : (∀ k in Finset.Icc 1, n + (1 : ℛ) ^ 2 ^ k) < 5 / 2 := by induction n with | zero => contradiction | succ n hh => cases n with | zero => norm_num #1 | succ n => induction k with | zero => norm_num | succ k ih => [Finset.prod_Icc succ top] at hn h₀ => linarith | succ k => simp_all [Finset.prod_Icc succ top, pow_succ, mul_comm] linarith | succ n => simp_all [Finset.prod_Icc succ top, Nat.cast_succ, div_eq_mul_inv] norm_num #2 ring_nf linarith ``` * The initial lines are identical to the left snippet. * The key difference is within the `succ n hh` case. Instead of directly applying simplification rules, it introduces an inner `induction k with ...` * **Inner Base Case:** `zero => norm_num` * **Inner Inductive Step:** `succ k ih => [Finset.prod_Icc succ top] at hn h₀ => linarith` and `succ k => simp_all [Finset.prod_Icc succ top, pow_succ, mul_comm] linarith` * The original simplification steps from the left snippet are also present, but nested within the inner inductive step. ### Key Observations * The "LLM + APOLLO" snippet appears to be a more refined or expanded version of the "LLM" snippet. * The addition of the inner `induction k with` suggests that APOLLO introduces an additional level of inductive reasoning within the proof. * The use of `at hn h₀` indicates that the `Finset.prod_Icc succ top` lemma is being applied to hypotheses `hn` and `h₀`. * The `#1` and `#2` annotations next to `norm_num` likely refer to specific normalization tactics or lemmas. ### Interpretation The image demonstrates a potential workflow in automated theorem proving. The "LLM" snippet represents an initial attempt at proving the theorem, while "LLM + APOLLO" shows a refined proof strategy. APOLLO seems to enhance the proof by introducing an inner inductive step, potentially breaking down the problem into smaller, more manageable subproblems. This suggests that APOLLO acts as a proof search engine or tactic selector, guiding the LLM towards a more complete and efficient proof. The difference in code length and complexity highlights the added reasoning capability provided by APOLLO. The annotations (`#1`, `#2`) suggest that the system is utilizing specific normalization procedures during the proof process. The overall data suggests a system where an LLM generates a proof, and APOLLO refines it through additional reasoning steps.

\n ## Diagram: Side-by-Side Code Comparison (LLM vs. LLM + APOLLO) ### Overview The image displays a side-by-side comparison of two blocks of formal mathematical proof code written in the Lean 4 language. The left panel, titled "LLM" in a red header, shows a proof generated by a Large Language Model. The right panel, titled "LLM + APOLLO" in a green header, shows a more detailed and structured proof, presumably generated or enhanced by a system called APOLLO. The comparison highlights differences in proof strategy, detail, and the use of automated tactics. ### Components/Axes The image is divided into two vertical panels of equal width. **Left Panel (LLM):** * **Header:** A red rectangular box at the top containing the text "LLM". * **Code Block:** A block of Lean 4 code on a light pink background. * **Annotations:** Two highlighted sections in pink, labeled `#1` and `#2`. **Right Panel (LLM + APOLLO):** * **Header:** A green rectangular box at the top containing the text "LLM + APOLLO". * **Code Block:** A block of Lean 4 code on a light green background. * **Annotations:** Two highlighted sections in green, labeled `#1` and `#2`. The `#1` annotation is significantly more extensive than its counterpart on the left. ### Detailed Analysis **1. Common Code Structure (Both Panels):** Both proofs begin with identical setup lines: ```lean import Mathlib import Aesop set_option maxHeartbeats 0 open BigOperators Real Nat Topology Rat theorem induction_pord1p1on2powklt5on2_llm (n k : ℕ) (h₀ : 0 < n) : (∏ k in Finset.Icc 1 n, 1 + (1 : ℝ) / 2 ^ k) < 5 / 2 := by ``` This defines a theorem named `induction_pord1p1on2powklt5on2_llm` (the right panel uses `_apollo`). The theorem states that for natural numbers `n` and `k`, with the hypothesis `h₀ : 0 < n`, the product of the terms `(1 + 1/2^k)` for `k` from 1 to `n` is strictly less than 5/2. **2. Proof Strategy - Left Panel (LLM):** The proof proceeds by induction on `n`. ```lean induction n with | zero => contradiction | succ n hn => cases n with | zero => norm_num #1 -- Annotation #1 | succ n => simp_all [Finset.prod_Icc_succ_top, Nat.cast_succ, div_eq_mul_inv] norm_num #2 -- Annotation #2 ring_nf linarith ``` * **Base Case (`zero`):** Discharged by `contradiction` (since `h₀ : 0 < 0` is false). * **Inductive Step (`succ n hn`):** Uses `cases n` to split into two subcases. * Subcase `zero` (i.e., `n=1`): Uses `norm_num` (Annotation #1) to verify the numeric inequality. * Subcase `succ n` (i.e., `n ≥ 2`): Uses `simp_all` with specific lemmas, then `norm_num` (Annotation #2), `ring_nf` for normalization, and `linarith` for linear arithmetic. **3. Proof Strategy - Right Panel (LLM + APOLLO):** The proof also begins with induction on `n` but introduces a nested induction on `k` within the inductive step. ```lean induction n with | zero => contradiction | succ n hn => cases n with | zero => norm_num induction k with -- Nested induction begins | zero => norm_num [Finset.prod_Icc_succ_top] at hn h₀ <;> linarith | succ k ih => cases k with | zero => norm_num [Finset.prod_Icc_succ_top] at hn h₀ <;> linarith | succ k => simp_all [Finset.prod_Icc_succ_top, pow_succ, mul_comm] linarith -- End of nested induction block (Annotation #1) | succ n => simp_all [Finset.prod_Icc_succ_top, Nat.cast_succ, div_eq_mul_inv] norm_num #2 -- Annotation #2 ring_nf linarith ``` * **Base Case (`zero`):** Identical to the left panel. * **Inductive Step (`succ n hn`):** Uses `cases n`. * Subcase `zero` (i.e., `n=1`): This is where the major difference lies (Annotation #1). Instead of a single `norm_num`, it performs a **nested induction on `k`**. This inner induction has its own base case (`zero`) and inductive step (`succ k ih`), which is further split. This suggests a more granular, step-by-step verification of the product inequality for the specific case where `n=1`, possibly to handle the product over `k` more explicitly. * Subcase `succ n` (i.e., `n ≥ 2`): The code is identical to the left panel's corresponding subcase, including Annotation #2. **4. Annotations:** * **Annotation #1 (Left - LLM):** A single tactic: `norm_num`. * **Annotation #1 (Right - LLM + APOLLO):** A multi-line block implementing a nested induction on `k` with several tactics (`norm_num`, `induction`, `cases`, `simp_all`, `linarith`). This is the core differentiator. * **Annotation #2 (Both Panels):** Identical in both: `norm_num`. ### Key Observations 1. **Structural Divergence:** The primary difference is in the subcase where `n=1`. The LLM proof uses a single tactic, while the LLM+APOLLO proof expands this into a detailed nested induction on the product index `k`. 2. **Proof Granularity:** The APOLLO-enhanced proof is more verbose and structured, breaking down the problem further. This may indicate a strategy to increase proof reliability or provide more detailed steps for verification. 3. **Identical Core Logic:** For the base case (`n=0`) and the inductive subcase for `n ≥ 2`, the proofs are identical. The enhancement is localized to a specific, potentially tricky part of the proof. 4. **Use of Tactics:** Both proofs use a similar set of Lean tactics (`induction`, `cases`, `norm_num`, `simp_all`, `linarith`), but APOLLO's version uses them in a more nested and explicit sequence. ### Interpretation This diagram illustrates a comparison between a standard LLM-generated formal proof and one augmented by a system named APOLLO. The key takeaway is that **APOLLO appears to enhance the proof by introducing more detailed, structured reasoning in complex subgoals.** * **What the data suggests:** The LLM alone produced a correct but minimally detailed proof for the `n=1` case. The APOLLO system identified this as a point requiring deeper justification and automatically generated a nested induction on `k` to provide that justification. This suggests APOLLO may function as a **proof refinement or debugging tool**, expanding high-level tactic calls into more fundamental steps. * **How elements relate:** The two panels are direct counterparts. The identical headers and theorem names establish they are solving the same problem. The divergence in the `| zero =>` subcase under `| succ n hn =>` is the focal point, demonstrating APOLLO's intervention. * **Notable patterns/anomalies:** The most significant pattern is the transformation of a single `norm_num` tactic into a multi-step inductive argument. This is not an error but a deliberate enrichment of the proof. It implies that for full formal verification or educational purposes, the APOLLO-style proof is more robust and transparent, as it leaves fewer steps to automated "black box" tactics. The fact that the rest of the proof remains unchanged suggests APOLLO's modifications are targeted and context-aware.

## Code Comparison: LLM vs LLM + APOLLO ### Overview The image shows two side-by-side code snippets implementing a mathematical theorem proof using Lean 4 syntax. The left snippet is labeled "LLM" (red header), and the right is labeled "LLM + APOLLO" (green header). Both implement the same theorem (`induction_pord1p1on2powklt5on2_...`) but differ in proof structure and auxiliary lemmas. ### Components/Axes - **Headers**: - Red header: "LLM" - Green header: "LLM + APOLLO" - **Imports**: - Both import `Mathlib` and `Aesop`. - **Options**: - `set_option maxHeartbeats 0` (disables interactive mode). - **Open Statements**: - `open BigOperators Real Nat Topology Rat` (exposes mathematical libraries). - **Theorem Declaration**: - Theorem name: `induction_pord1p1on2powklt5on2_...` - Parameters: `(n k : ℕ)` (natural numbers `n` and `k`). - Hypothesis: `(h₀ : 0 < n)` (natural number `n` is positive). - **Proof Structure**: - Both use induction on `n` with contradiction. - Case analysis on `n` (zero vs successor). - Differences in auxiliary lemmas and proof tactics. ### Detailed Analysis #### LLM (Left Snippet) - **Proof Steps**: 1. **Base Case**: `n = 0` → `contradiction` (no explicit handling). 2. **Successor Case**: `n = succ n` → - Applies `simp_all` with `[Finset.prod_Icc_succ_top, Nat.cast_succ, div_eq_mul_inv]`. - Uses `norm_num` (automated normalization) and `ring_nf` (ring normalization). - Final step: `linarith` (linear arithmetic). - **Key Lemmas**: - `Finset.prod_Icc_succ_top` (product over intervals). - `Nat.cast_succ` (natural number successor casting). - `div_eq_mul_inv` (division equivalence). #### LLM + APOLLO (Right Snippet) - **Proof Steps**: 1. **Base Case**: `n = 0` → `contradiction`. 2. **Successor Case**: `n = succ n` → - Applies `simp_all` with `[Finset.prod_Icc_succ_top, pow_succ, mul_comm]`. - Uses `norm_num` and `ring_nf`. - Final step: `linarith`. - **Additional Tactics**: - Explicit induction on `k` with `induction k with | zero => norm_num`. - Uses `Finset.prod_Icc_succ_top` at `hn h₀` (hypothesis context). - Applies `mul_comm` (commutativity of multiplication). ### Key Observations 1. **Theorem Parameters**: - Both use `(n k : ℕ)`, but the Apollo version adds a closing parenthesis (`n k: ℕ)`). 2. **Proof Differences**: - Apollo version introduces induction on `k` and uses `pow_succ`/`mul_comm` instead of `Nat.cast_succ`/`div_eq_mul_inv`. - Apollo proof includes explicit handling of `k` in the successor case. 3. **Lemma Usage**: - LLM relies on `div_eq_mul_inv`; Apollo uses `mul_comm`. - Apollo adds `ring_nf` in both snippets but with different contexts. ### Interpretation The APOLLO extension appears to optimize the proof by: 1. **Modularizing Induction**: Inducting on both `n` and `k` (vs. only `n` in LLM). 2. **Simplifying Arithmetic**: Using `pow_succ` (power successor) and `mul_comm` to reduce case complexity. 3. **Contextual Simplification**: Applying lemmas like `Finset.prod_Icc_succ_top` at specific hypothesis contexts (`hn h₀`). The APOLLO version likely improves proof efficiency by breaking down the problem into smaller, reusable components (e.g., induction on `k`), whereas the LLM version handles everything in a single inductive step. The use of `ring_nf` and `linarith` in both suggests reliance on Lean’s automated ring and linear arithmetic solvers. **Note**: The code uses Lean 4’s type theory syntax (e.g., `ℕ` for natural numbers, `succ` for successor). No non-English text is present.