## Code Comparison: LLM vs. LLM + APOLLO ### Overview The image presents a side-by-side comparison of code snippets, one labeled "LLM" and the other "LLM + APOLLO". Both snippets appear to be related to mathematical theorem proving, likely using a formal verification system. The comparison highlights differences in the code required to prove a specific theorem using two different approaches. ### Components/Axes * **Left Block:** * Title: "LLM" (red background) * Code: A series of commands and a theorem definition. * **Right Block:** * Title: "LLM + APOLLO" (green background) * Code: A series of commands and a theorem definition. ### Detailed Analysis or ### Content Details **Left Block (LLM):** * `import Mathlib` * `import Aesop` * `set_option maxHeartbeats 0` * `open BigOperators Real Nat Topology Rat` * `theorem imo_1983_p6_llm (a b c : R) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : c < a + b) (h₂ : b < a + c) (h₃ : a < b + c) : 0 ≤ a ^ 2 * b * (a - b) + b ^ 2 * c * (b - c) + c ^ 2 * a * (c - a) := by` * `nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), mul_pos h₀.left h₀.right.left, mul_pos h₀.left h₀.right.right, mul_pos h₀.right.left h₀.right.right]` * Annotation: "#1" next to `sq_nonneg (b - c)` in the `nlinarith` line. **Right Block (LLM + APOLLO):** * `import Mathlib` * `import Aesop` * `set_option maxHeartbeats 0` * `open BigOperators Real Nat Topology Rat` * `theorem imo_1983_p6_apollo (a b c : R) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : c < a + b) (h₂ : b < a + c) (h₃ : a < b + c) : 0 ≤ a ^ 2 * b * (a - b) + b ^ 2 * c * (b - c) + c ^ 2 * a * (c - a) := by` * `nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), mul_pos (sub_pos.mpr h₁), (sub_pos.mpr h₂), mul_pos (sub_pos.mpr h₂), (sub_pos.mpr h₃), mul_pos (sub_pos.mpr h₃ (sub_pos.mpr h₁)]` * Annotation: "#1" next to `sq_nonneg (b - c)` in the `nlinarith` line. ### Key Observations * Both code snippets define a theorem named `imo_1983_p6_llm` and `imo_1983_p6_apollo` respectively, which appears to be related to the International Mathematical Olympiad (IMO) problem from 1983, problem 6. * The theorem states that under certain conditions on real numbers `a`, `b`, and `c`, a specific inequality holds. * The `nlinarith` command is used to prove the theorem. This command likely invokes a linear arithmetic solver. * The key difference lies in the arguments passed to the `nlinarith` command. The "LLM" version requires more explicit hints (multiple repetitions of `sq_nonneg` and explicit calls to `mul_pos` with detailed arguments), while the "LLM + APOLLO" version uses a more concise and automated approach (using `sub_pos.mpr` and fewer explicit hints). ### Interpretation The image demonstrates the impact of using the "APOLLO" extension in conjunction with "LLM" for proving mathematical theorems. The "LLM + APOLLO" approach significantly simplifies the proof process by reducing the amount of manual guidance required for the linear arithmetic solver. This suggests that "APOLLO" provides a higher level of automation or more powerful reasoning capabilities compared to using "LLM" alone. The annotation "#1" likely refers to a specific point or step in the proof process that is being highlighted.

## Code Comparison Diagram: LLM vs. LLM + APOLLO Theorem Proving ### Overview This image is a side-by-side comparison of two code snippets written in the Lean 4 theorem proving language. It contrasts the output generated by a standard Large Language Model ("LLM") on the left with the output generated by an LLM augmented with a system called "APOLLO" on the right. Both snippets attempt to prove a mathematical theorem related to the International Mathematical Olympiad (IMO) 1983, Problem 6. The visual design uses color coding (red for the baseline LLM, green for the APOLLO-augmented LLM) to highlight the differences in the final proof tactic. ### Components & Layout The image is divided into two distinct rectangular panels of equal size: 1. **Left Panel (Red Theme):** * **Header:** A solid red rectangle at the top center containing the text "LLM" in black. * **Border:** A thick red outline surrounding the panel. * **Background:** The top portion has a very faint red/pink tint (almost white), while the bottom highlighted code block has a distinct light red background. * **Annotation:** A small, darker red square in the top-right corner of the highlighted block containing the text "#1" in white. 2. **Right Panel (Green Theme):** * **Header:** A solid green rectangle at the top center containing the text "LLM + APOLLO" in black. * **Border:** A thick green outline surrounding the panel. * **Background:** The top portion has a very faint green tint (almost white), while the bottom highlighted code block has a distinct light green background. * **Annotation:** A small, darker green square in the top-right corner of the highlighted block containing the text "#1" in black. ### Content Details Both panels share identical setup code and theorem declarations (with minor line-wrapping differences), but diverge significantly in the final `nlinarith` tactic block. #### Left Panel Transcription (LLM) ```lean import Mathlib import Aesop set_option maxHeartbeats 0 open BigOperators Real Nat Topology Rat theorem imo_1983_p6_llm (a b c : ℝ) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : c < a + b) (h₂ : b < a + c) (h₃ : a < b + c) : 0 ≤ a ^ 2 * b * (a - b) + b ^ 2 * c * (b - c) + c ^ 2 * a * (c - a) := by nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), mul_pos h₀.left h₀.right.left, mul_pos h₀.left h₀.right.right, mul_pos h₀.right.left h₀.right.right] ``` *(Note: The `nlinarith` block is highlighted in light red, with `#1` in the top right corner).* #### Right Panel Transcription (LLM + APOLLO) ```lean import Mathlib import Aesop set_option maxHeartbeats 0 open BigOperators Real Nat Topology Rat theorem imo_1983_p6_apollo (a b c : ℝ) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : c < a + b) (h₂ : b < a + c) (h₃ : a < b + c) : 0 ≤ a ^ 2 * b * (a - b) + b ^ 2 * c * (b - c) + c ^ 2 * a * (c - a) := by nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), mul_pos (sub_pos.mpr h₁) (sub_pos.mpr h₂), mul_pos (sub_pos.mpr h₂) (sub_pos.mpr h₃), mul_pos (sub_pos.mpr h₃) (sub_pos.mpr h₁)] ``` *(Note: The `nlinarith` block is highlighted in light green, with `#1` in the top right corner).* ### Key Observations * **Shared Context:** Both models correctly set up the environment (`import Mathlib`, `import Aesop`), set options (`maxHeartbeats 0`), and define the theorem signature for IMO 1983 Problem 6. The theorem involves real numbers $a, b, c$ that are strictly positive ($h_0$) and satisfy the triangle inequalities ($h_1, h_2, h_3$). * **Naming Convention:** The left theorem is named `imo_1983_p6_llm`, while the right is named `imo_1983_p6_apollo`. * **Divergence in Logic (The Highlighted Blocks):** * **The Baseline LLM (Red):** The arguments provided to the `nlinarith` (non-linear arithmetic) tactic contain redundancies. It repeats `sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a)` twice. Furthermore, it attempts to use `mul_pos` by combining the basic positivity hypotheses from $h_0$ (e.g., `h₀.left`, which is $0 < a$). * **The APOLLO LLM (Green):** The arguments are concise and mathematically distinct. It lists the `sq_nonneg` terms only once. Crucially, it uses `mul_pos` in conjunction with `sub_pos.mpr` applied to the triangle inequality hypotheses ($h_1, h_2, h_3$). For example, `sub_pos.mpr h₁` converts the hypothesis $c < a + b$ into the mathematically useful form $0 < a + b - c$. ### Interpretation This image serves as a demonstration of the efficacy of the "APOLLO" system in improving the formal mathematical reasoning capabilities of Large Language Models. The data suggests that a standard LLM (left) struggles to provide the correct auxiliary proofs required by the `nlinarith` tactic to close the goal. The baseline LLM exhibits "hallucination" or poor logical planning by repeating identical arguments and feeding basic, insufficient positivity proofs (`h₀`) into the tactic, which likely results in a failure to compile or prove the theorem. Conversely, the APOLLO-augmented system (right) demonstrates a deeper understanding of the mathematical requirements. It recognizes that to solve this specific non-linear inequality, the tactic needs to know that the terms derived from the triangle inequalities are positive. By applying `sub_pos.mpr` to $h_1, h_2,$ and $h_3$, APOLLO correctly transforms the hypotheses into the exact format required by `nlinarith` to successfully complete the proof. The use of red (often associated with failure/errors) and green (associated with success/correctness) strongly implies that the left code fails while the right code succeeds.

## Code Comparison: LLM vs. LLM + APOLLO ### Overview The image presents a side-by-side comparison of code generated by two systems: "LLM" (left) and "LLM + APOLLO" (right). Both systems appear to be using a formal verification or theorem proving environment, likely Coq, based on the syntax. The code snippets define a theorem `imo_1983_p6` and a related nlinarith proof. ### Components/Axes There are no axes or traditional chart components. The image consists of two distinct code blocks, each with a header indicating the system that generated it ("LLM" and "LLM + APOLLO"). Each code block contains the following elements: * `import` statements: `Mathlib` and `Aesop` * `set_option` statement: `maxHeartbeats 0` * `open` statement: `BigOperators Real Nat Topology Rat` * `theorem` definition: `imo_1983_p6` * `nlinarith` proof block: containing a series of constraints and operations. ### Detailed Analysis or Content Details **LLM (Left)** * **Imports:** `import Mathlib`, `import Aesop` * **Option:** `set_option maxHeartbeats 0` * **Open:** `open BigOperators Real Nat Topology Rat` * **Theorem:** `theorem imo_1983_p6_llm (a b c : R) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : c < a + b) (h₂ : b < a + c) (h₃ : a < b + c) : 0 ≤ a ^ 2 + b ^ 2 + c ^ 2 - 2 * c * (b - c) + c ^ 2 * a * (c - a) := by` * **nlinarith:** * `nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), mul_pos ho.left h₀.right, mul_pos ho.left h₁.right, mul_pos h₁.right.left h₀.right.right]` **LLM + APOLLO (Right)** * **Imports:** `import Mathlib`, `import Aesop` * **Option:** `set_option maxHeartbeats 0` * **Open:** `open BigOperators Real Nat Topology Rat` * **Theorem:** `theorem imo_1983_p6_apollo (a b c : R) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : c < a + b) (h₂ : b < a + c) (h₃ : a < b + c) : 0 ≤ a ^ 2 + b ^ 2 + c ^ 2 - 2 * c * (b - c) + c ^ 2 * a * (c - a) := by` * **nlinarith:** * `nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), mul_pos (sub_pos.mpr h₁) (sub_pos.mpr h₂), mul_pos (sub_pos.mpr h₂) (sub_pos.mpr h₃), mul_pos (sub_pos.mpr h₃) (sub_pos.mpr h₁)]` **Differences in nlinarith:** The key difference lies within the `nlinarith` block. The "LLM" version uses `mul_pos ho.left h₀.right`, `mul_pos ho.left h₁.right`, and `mul_pos h₁.right.left h₀.right.right`. The "LLM + APOLLO" version uses `mul_pos (sub_pos.mpr h₁) (sub_pos.mpr h₂)` and similar constructions involving `sub_pos.mpr`. This suggests that APOLLO is introducing a step to explicitly prove the positivity of the differences before multiplying, potentially leading to a more robust or complete proof. ### Key Observations The code is nearly identical between the two systems, except for the `nlinarith` block. The "LLM + APOLLO" version appears to be more verbose and explicit in its reasoning, using `sub_pos.mpr` to demonstrate the positivity of terms before applying `mul_pos`. This could indicate that APOLLO is adding a layer of proof automation or simplification. ### Interpretation The image demonstrates a comparison between a baseline LLM and an LLM augmented with APOLLO for formal verification. The theorem `imo_1983_p6` likely represents a mathematical inequality. The difference in the `nlinarith` blocks suggests that APOLLO is enhancing the LLM's ability to generate proofs by adding more explicit reasoning steps. The use of `sub_pos.mpr` indicates that APOLLO is actively verifying the positivity of terms, which is crucial for the correctness of the proof. This suggests that APOLLO is not simply generating code, but also contributing to the proof strategy itself. The `maxHeartbeats 0` setting suggests that the systems are configured to avoid timeouts during proof search. The fact that both systems produce valid code (at least syntactically) indicates that the LLM has a good understanding of the Coq syntax and semantics. The addition of APOLLO appears to refine the proof process, potentially making it more reliable and complete.

\n ## Code Comparison Diagram: LLM vs. LLM + APOLLO Proof Scripts ### Overview The image displays a side-by-side comparison of two Lean 4 code blocks. The left block, outlined in red, is labeled "LLM". The right block, outlined in green, is labeled "LLM + APOLLO". Both blocks contain code to prove the same mathematical theorem (`imo_1983_p6`), but they employ different proof tactics, suggesting a comparison of proof strategies or the effect of an additional tool (APOLLO). ### Components/Axes The image is divided into two primary, vertically-aligned rectangular regions: 1. **Left Region (LLM):** Bordered in red. Contains a complete Lean 4 proof script. 2. **Right Region (LLM + APOLLO):** Bordered in green. Contains a complete Lean 4 proof script. Each region contains the following structural components: * **Header Label:** A colored box at the top center of each region ("LLM" in red, "LLM + APOLLO" in green). * **Code Block:** Monospaced text representing Lean 4 code. * **Highlighted Proof Tactic:** The final `nlinarith` tactic call is highlighted with a background color matching the region's border (light red on the left, light green on the right). A small tag `#1` appears at the end of the first line of this tactic in both blocks. ### Detailed Analysis / Content Details **1. Common Code Structure (Both Blocks):** Both scripts share identical setup and theorem statements: ```lean import Mathlib import Aesop set_option maxHeartbeats 0 open BigOperators Real Nat Topology Rat theorem imo_1983_p6_... (a b c : ℝ) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : c < a + b) (h₂ : b < a + c) (h₃ : a < b + c) : 0 ≤ a ^ 2 * b * (a - b) + b ^ 2 * c * (b - c) + c ^ 2 * a * (c - a) := by ``` * **Imports:** `Mathlib`, `Aesop`. * **Option:** `maxHeartbeats` set to 0 (disabling the timeout). * **Opened Namespaces:** `BigOperators`, `Real`, `Nat`, `Topology`, `Rat`. * **Theorem Hypotheses:** `a, b, c` are positive real numbers (`h₀`), and they satisfy the triangle inequalities (`h₁`, `h₂`, `h₃`). * **Theorem Conclusion:** A specific cyclic inequality involving squares and products of `a, b, c`. **2. Divergent Proof Tactics (The Key Difference):** The proof scripts differ entirely in the tactic used after `:= by`. * **Left Block (LLM) Proof Tactic:** ```lean nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), mul_pos h₀.left h₀.right.left, mul_pos h₀.left h₀.right.right, mul_pos h₀.right.left h₀.right.right] ``` * **Tactic:** `nlinarith` (non-linear arithmetic). * **Provided Facts:** A list of 9 facts: 1. `sq_nonneg (a - b)` (repeated twice) 2. `sq_nonneg (b - c)` (repeated twice) 3. `sq_nonneg (c - a)` (repeated twice) 4. `mul_pos h₀.left h₀.right.left` (product of `a>0` and `b>0` is positive) 5. `mul_pos h₀.left h₀.right.right` (product of `a>0` and `c>0` is positive) 6. `mul_pos h₀.right.left h₀.right.right` (product of `b>0` and `c>0` is positive) * **Right Block (LLM + APOLLO) Proof Tactic:** ```lean nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), mul_pos (sub_pos.mpr h₁) (sub_pos.mpr h₂), mul_pos (sub_pos.mpr h₂) (sub_pos.mpr h₃), mul_pos (sub_pos.mpr h₃) (sub_pos.mpr h₁)] ``` * **Tactic:** `nlinarith` (non-linear arithmetic). * **Provided Facts:** A list of 6 facts: 1. `sq_nonneg (a - b)` 2. `sq_nonneg (b - c)` 3. `sq_nonneg (c - a)` 4. `mul_pos (sub_pos.mpr h₁) (sub_pos.mpr h₂)` (product of `(a+b-c)>0` and `(a+c-b)>0` is positive) 5. `mul_pos (sub_pos.mpr h₂) (sub_pos.mpr h₃)` (product of `(a+c-b)>0` and `(b+c-a)>0` is positive) 6. `mul_pos (sub_pos.mpr h₃) (sub_pos.mpr h₁)` (product of `(b+c-a)>0` and `(a+b-c)>0` is positive) ### Key Observations 1. **Identical Goal:** Both proofs aim to establish the same inequality under the same hypotheses. 2. **Proof Strategy Divergence:** The core difference lies in the auxiliary facts supplied to the `nlinarith` automation tactic. 3. **Fact Selection - LLM:** The LLM proof uses a redundant set of non-negativity facts for squares (`sq_nonneg`) and basic positivity facts derived directly from `h₀` (`a,b,c > 0`). 4. **Fact Selection - LLM + APOLLO:** The APOLLO-assisted proof uses a more targeted set. It includes the three necessary `sq_nonneg` facts without repetition. Crucially, it derives positivity facts from the *triangle inequalities* (`h₁, h₂, h₃`) using `sub_pos.mpr`, which transforms `c < a + b` into `0 < a + b - c`. The supplied `mul_pos` facts are products of these derived positive terms. 5. **Conciseness:** The APOLLO version provides fewer total facts (6 vs. 9) and avoids redundancy. ### Interpretation This diagram illustrates a comparison between two automated theorem proving approaches for a classic IMO problem. The "LLM" label suggests a baseline proof generated by a Large Language Model. The "LLM + APOLLO" label indicates a proof where the LLM's output is augmented or guided by a system named APOLLO. The key insight is in the **quality and relevance of the auxiliary facts** fed to the `nlinarith` tactic. The LLM-generated proof uses a somewhat brute-force approach, supplying many basic, loosely related facts (including duplicates). In contrast, the APOLLO-assisted proof demonstrates a more sophisticated understanding of the problem structure. It correctly identifies that the triangle inequalities (`h₁, h₂, h₃`) are the critical source of positivity for the terms `(a+b-c)`, `(a+c-b)`, and `(b+c-a)`, which are central to the inequality's proof. By providing these derived facts, the APOLLO system likely makes the `nlinarith` tactic's job more efficient and direct. Therefore, the image suggests that APOLLO enhances the LLM's capability by improving its **strategic selection of lemmas** or its ability to **perform intermediate reasoning steps** (like applying `sub_pos.mpr`) before invoking automation. This leads to a more elegant, concise, and logically focused proof script. The comparison highlights the difference between generating syntactically correct code and generating optimally informative code for automated provers.

## Code Comparison: LLM vs. LLM + APOLLO ### Overview The image presents two side-by-side code snippets written in a formal proof assistant (likely Coq, given imports like `Mathlib` and `Aesop`). Both snippets define theorems related to real number inequalities and use `nlinarith` (nonlinear arithmetic) to prove them. The left snippet is labeled "LLM," and the right "LLM + APOLLO," suggesting a comparison of proof strategies or tools. --- ### Components/Axes #### Common Elements: - **Imports**: - `Mathlib` (core mathematical library) - `Aesop` (likely a custom or third-party library for arithmetic reasoning) - **Global Option**: - `set_option maxHeartbeats 0` (disables interactive proof search) - **Open Scope**: - `BigOperators Real Nat Topology Rat` (enables reasoning with real numbers, natural numbers, and rational numbers) #### Differences: 1. **Theorem Names**: - Left: `imo_1983_p6_llm` - Right: `imo_1983_p6_apollo` 2. **Hypotheses**: - Both share `h0 : 0 < a ∧ 0 < b ∧ 0 < c`, `h1 : c < a + b`, `h2 : b < a + c`. - Right adds `h3 : a < b + c` (triangle inequality for all pairs). 3. **Conclusion**: - Left: `0 ≤ a * 2 * b * (a - b) + b * 2 * c * (b - c) + c * 2 * a * (c - a)` - Right: `2 * c * (b - c) + c * 2 * a * (c - a)` (simplified form). #### nlinarith Blocks: - **Left (LLM)**: - Uses `sq_nonneg` (square non-negativity) and `mul_pos` (multiplicative positivity) with explicit term decomposition. - Example: `mul_pos h0.left h0.right.left` (applies positivity to subterms). - **Right (LLM + APOLLO)**: - Uses `sub_pos` (subtraction positivity) and nested `mul_pos` with subterm extraction. - Example: `mul_pos (sub_pos.mpr h1) (sub_pos.mpr h2)` (applies positivity to differences). --- ### Detailed Analysis #### Theorem Structure: - **LLM**: - Proves a cyclic inequality involving products of differences (e.g., `a * (a - b)`). - Relies on `sq_nonneg` to handle squared terms and `mul_pos` for positivity. - **LLM + APOLLO**: - Simplifies the conclusion to a linear combination of differences. - Uses `sub_pos` to directly reason about differences (e.g., `b - c`) and combines them multiplicatively. #### Key Differences in nlinarith: - **LLM**: - Explicitly decomposes terms into subcomponents (e.g., `h0.left`, `h0.right`). - Focuses on individual term positivity. - **LLM + APOLLO**: - Leverages `sub_pos` to handle differences first, then applies multiplicative positivity. - Reduces redundancy by reusing subterm proofs (e.g., `sub_pos.mpr h1`). --- ### Key Observations 1. **Hypothesis Expansion**: - The APOLLO version includes `h3 : a < b + c`, ensuring all triangle inequalities are satisfied, which may simplify the proof. 2. **Simplified Conclusion**: - The right-hand side of the APOLLO theorem is a linear expression, whereas the LLM version is quadratic. This suggests APOLLO’s strategy avoids unnecessary complexity. 3. **Proof Strategy**: - APOLLO uses `sub_pos` to directly reason about differences, while LLM relies on squaring terms to enforce non-negativity. --- ### Interpretation The comparison highlights how the APOLLO extension enhances the LLM’s reasoning capabilities: - **Efficiency**: APOLLO’s use of `sub_pos` reduces the need for term decomposition, streamlining the proof. - **Generality**: By including `h3`, APOLLO ensures symmetry in the triangle inequality, making the conclusion more robust. - **Tooling**: The APOLLO version likely integrates advanced arithmetic tactics (e.g., `mul_pos` with subterm extraction), enabling more concise proofs. This suggests that APOLLO improves upon LLM’s approach by combining stronger hypotheses and more sophisticated arithmetic reasoning, potentially reducing proof length and complexity.