## Chart: Theorems Proved vs. Wall-Clock Time ### Overview The image is a line chart comparing the number of theorems proved by different systems (COPRA and ReProver) using different configurations (with and without retrieval) over a period of wall-clock time in seconds. The chart displays four data series, each representing a different system configuration. ### Components/Axes * **Title:** pass@n-seconds * **X-axis:** Wall-Clock Time in Seconds (n) * Scale: 0 to 600, with tick marks at intervals of 100. * **Y-axis:** Number of Theorems Proved * Scale: 0 to 70, with tick marks at intervals of 10. * **Legend:** Located in the center-right of the chart. * **Gold:** COPRA (GPT-4-turbo) (with Retrieval) * **Dark Blue:** ReProver (with Retrieval) * **Green:** COPRA (GPT-4) (without Retrieval) * **Red:** ReProver (without Retrieval) ### Detailed Analysis * **COPRA (GPT-4-turbo) (with Retrieval) - Gold Line:** * Trend: The line generally slopes upward, indicating an increase in the number of theorems proved as time increases. The line plateaus around 65 theorems proved after approximately 300 seconds. * Data Points: * At approximately 100 seconds, around 50 theorems proved. * At approximately 200 seconds, around 60 theorems proved. * At approximately 300 seconds, around 65 theorems proved. * At approximately 600 seconds, around 65 theorems proved. * **ReProver (with Retrieval) - Dark Blue Line:** * Trend: The line slopes upward, indicating an increase in the number of theorems proved as time increases. * Data Points: * At approximately 100 seconds, around 2 theorems proved. * At approximately 200 seconds, around 20 theorems proved. * At approximately 300 seconds, around 35 theorems proved. * At approximately 400 seconds, around 43 theorems proved. * At approximately 500 seconds, around 54 theorems proved. * At approximately 600 seconds, around 61 theorems proved. * **COPRA (GPT-4) (without Retrieval) - Green Line:** * Trend: The line increases rapidly initially, then plateaus around 65 theorems proved after approximately 200 seconds. * Data Points: * At approximately 50 seconds, around 48 theorems proved. * At approximately 100 seconds, around 58 theorems proved. * At approximately 200 seconds, around 62 theorems proved. * At approximately 600 seconds, around 65 theorems proved. * **ReProver (without Retrieval) - Red Line:** * Trend: The line slopes upward, indicating an increase in the number of theorems proved as time increases. * Data Points: * At approximately 100 seconds, around 2 theorems proved. * At approximately 200 seconds, around 5 theorems proved. * At approximately 300 seconds, around 25 theorems proved. * At approximately 400 seconds, around 43 theorems proved. * At approximately 500 seconds, around 50 theorems proved. * At approximately 600 seconds, around 54 theorems proved. ### Key Observations * COPRA (GPT-4) without retrieval (green line) proves theorems much faster initially than the other configurations, reaching a plateau early on. * COPRA (GPT-4-turbo) with retrieval (gold line) performs similarly to COPRA (GPT-4) without retrieval (green line), but plateaus slightly earlier. * ReProver, both with and without retrieval (blue and red lines), proves theorems at a slower rate compared to COPRA. * The "with Retrieval" configurations for both COPRA and ReProver generally outperform their "without Retrieval" counterparts, although the difference is more pronounced for ReProver. ### Interpretation The chart demonstrates the performance of different theorem proving systems (COPRA and ReProver) under varying conditions (with and without retrieval). The data suggests that: * COPRA, especially when using GPT-4 (with or without retrieval), is more efficient at proving theorems within the given time frame compared to ReProver. * The use of retrieval mechanisms generally improves the performance of both systems, particularly for ReProver. * The rapid initial increase in theorems proved by COPRA (GPT-4) without retrieval suggests that it quickly finds a set of provable theorems and then plateaus, possibly indicating a limitation in its ability to explore more complex theorems without retrieval assistance. * The slower but more consistent increase in theorems proved by ReProver suggests a different approach to theorem proving, potentially one that explores a broader range of theorems but at a slower pace.

## Line Chart: pass@n-seconds ### Overview The image presents a line chart comparing the performance of two theorem proving systems, COPRAGPT-4-turbo and ReProver, with and without retrieval augmentation, measured by the number of theorems proved over time. The chart displays the cumulative number of theorems proven as a function of wall-clock time in seconds. ### Components/Axes * **Title:** pass@n-seconds (positioned at the top-center) * **X-axis:** Wall-Clock Time in Seconds (n) - ranging from approximately 0 to 600 seconds. * **Y-axis:** Number of Theorems Proved - ranging from 0 to 70. * **Legend:** Located in the top-right corner, listing the following data series: * COPRA (GPT-4-turbo) (with Retrieval) - Yellow * ReProver (with Retrieval) - Blue * COPRA (GPT-4) (without Retrieval) - Green * ReProver (without Retrieval) - Red ### Detailed Analysis The chart shows the cumulative number of theorems proven by each system over time. * **COPRA (GPT-4-turbo) (with Retrieval) - Yellow:** This line starts at approximately 0 theorems at 0 seconds and steadily increases, reaching approximately 68 theorems at around 400 seconds, and plateaus. * **ReProver (with Retrieval) - Blue:** This line also starts at 0 theorems at 0 seconds. It increases more slowly than the yellow line initially, but then accelerates, reaching approximately 55 theorems at around 400 seconds, and plateaus. * **COPRA (GPT-4) (without Retrieval) - Green:** This line starts at 0 theorems at 0 seconds and increases at a moderate pace, reaching approximately 60 theorems at around 350 seconds, and plateaus. * **ReProver (without Retrieval) - Red:** This line starts at 0 theorems at 0 seconds and increases very slowly initially. It begins to accelerate around 200 seconds, reaching approximately 45 theorems at 500 seconds. Approximate Data Points (extracted by visually estimating from the chart): | Time (seconds) | COPRA (GPT-4-turbo) (with Retrieval) | ReProver (with Retrieval) | COPRA (GPT-4) (without Retrieval) | ReProver (without Retrieval) | |---|---|---|---|---| | 0 | 0 | 0 | 0 | 0 | | 50 | 10 | 5 | 8 | 2 | | 100 | 20 | 10 | 15 | 5 | | 200 | 40 | 20 | 30 | 10 | | 300 | 55 | 35 | 45 | 20 | | 400 | 68 | 55 | 60 | 35 | | 500 | 68 | 55 | 60 | 45 | | 600 | 68 | 55 | 60 | 45 | ### Key Observations * COPRA (GPT-4-turbo) with retrieval consistently outperforms all other methods in terms of the number of theorems proven within the first 400 seconds. * ReProver with retrieval performs better than ReProver without retrieval, indicating the benefit of retrieval augmentation. * COPRA (GPT-4) without retrieval performs better than ReProver with and without retrieval. * ReProver without retrieval is the slowest to prove theorems. * All lines appear to plateau after approximately 400 seconds, suggesting diminishing returns in theorem proving performance with increased time. ### Interpretation The data suggests that COPRA (GPT-4-turbo) with retrieval is the most effective theorem proving system among those tested, demonstrating a significantly higher rate of theorem proving compared to the other methods. The consistent improvement observed when using retrieval augmentation across both COPRA and ReProver indicates that providing relevant information to the theorem provers enhances their performance. The plateauing of all lines suggests that there is a limit to the number of theorems that can be proven within the given timeframe, potentially due to the complexity of the remaining theorems or the inherent limitations of the systems. The differences in performance between the systems could be attributed to variations in their underlying algorithms, training data, or computational resources. The chart provides valuable insights into the effectiveness of different theorem proving approaches and the benefits of incorporating retrieval augmentation.

\n ## Line Chart: pass@n-seconds ### Overview The image is a line chart titled "pass@n-seconds" that compares the performance of four different automated theorem-proving systems over time. The chart plots the cumulative number of theorems proved against the wall-clock time in seconds. It demonstrates how quickly each system can solve problems, with a focus on the impact of a "Retrieval" mechanism. ### Components/Axes * **Chart Title:** `pass@n-seconds` (Top center) * **Y-Axis:** Label is `Number of Theorems Proved`. Scale runs from 0 to 70 in increments of 10. * **X-Axis:** Label is `Wall-Clock Time in Seconds (n)`. Scale runs from 0 to 600 in increments of 100. * **Legend:** Located in the bottom-right quadrant of the chart area. It contains four entries, each with a colored line sample and a text label: 1. **Yellow Line:** `COPRA (GPT-4-turbo) (with Retrieval)` 2. **Blue Line:** `ReProver (with Retrieval)` 3. **Green Line:** `COPRA (GPT-4) (without Retrieval)` 4. **Red Line:** `ReProver (without Retrieval)` ### Detailed Analysis The chart displays four data series, each representing a different system configuration. The trend for each is a non-decreasing step function, as the cumulative count of proved theorems can only increase or stay flat. 1. **COPRA (GPT-4-turbo) with Retrieval (Yellow Line):** * **Trend:** Shows the fastest initial growth and maintains the highest performance throughout. It has a very steep ascent in the first ~50 seconds, then continues to climb in smaller steps, plateauing near the top. * **Key Data Points (Approximate):** * At n=50s: ~50 theorems proved. * At n=100s: ~55 theorems proved. * At n=300s: ~64 theorems proved. * At n=600s: ~71 theorems proved (highest final value). 2. **COPRA (GPT-4) without Retrieval (Green Line):** * **Trend:** Follows a very similar trajectory to its "with Retrieval" counterpart (yellow), but consistently lags slightly behind. It also has a steep initial rise. * **Key Data Points (Approximate):** * At n=50s: ~49 theorems proved. * At n=100s: ~53 theorems proved. * At n=300s: ~62 theorems proved. * At n=600s: ~65 theorems proved. 3. **ReProver with Retrieval (Blue Line):** * **Trend:** Begins proving theorems later than the COPRA systems (starting around n=100s). It shows a steady, roughly linear increase over time, with a moderate slope. * **Key Data Points (Approximate):** * At n=100s: ~5 theorems proved. * At n=200s: ~18 theorems proved. * At n=300s: ~35 theorems proved. * At n=600s: ~61 theorems proved. 4. **ReProver without Retrieval (Red Line):** * **Trend:** Also begins around n=100s. Its growth is the slowest of the four, with a shallower slope compared to the blue line (ReProver with Retrieval). * **Key Data Points (Approximate):** * At n=100s: ~2 theorems proved. * At n=200s: ~14 theorems proved. * At n=300s: ~33 theorems proved. * At n=600s: ~54 theorems proved. ### Key Observations * **Performance Hierarchy:** The final ranking at 600 seconds is: 1) COPRA (GPT-4-turbo, with Retrieval), 2) COPRA (GPT-4, without Retrieval), 3) ReProver (with Retrieval), 4) ReProver (without Retrieval). * **Impact of Retrieval:** For both COPRA and ReProver, the "with Retrieval" variant outperforms the "without Retrieval" variant. The performance gap is more pronounced for ReProver (blue vs. red lines) than for COPRA (yellow vs. green lines). * **Initial Speed:** The COPRA systems (yellow, green) demonstrate a significant advantage in the early phase (0-100 seconds), solving many theorems very quickly. The ReProver systems (blue, red) have a delayed start. * **Growth Patterns:** COPRA systems show a "fast start, then plateau" pattern. ReProver systems show a "slow start, then steady climb" pattern. ### Interpretation This chart evaluates the efficiency of different AI-driven theorem-proving agents. The data suggests that: 1. **Model Foundation Matters:** Systems built on GPT-4-turbo (COPRA) have a substantial initial speed and overall capacity advantage over the ReProver architecture in this benchmark. 2. **Retrieval is Beneficial:** Augmenting a prover with a retrieval mechanism (likely for accessing relevant lemmas or past proofs) consistently improves performance, allowing it to prove more theorems within the same time budget. This effect is critical for ReProver to become competitive. 3. **Time-Accuracy Trade-off:** If the goal is to solve as many problems as possible under a strict time limit (e.g., <100 seconds), COPRA is the clear choice. If given a longer time budget (>300 seconds), the gap narrows, and ReProver with Retrieval becomes a viable contender, eventually surpassing COPRA without Retrieval. 4. **Underlying Capability:** The steep initial climb of COPRA implies it may be better at recognizing and solving "easy" theorems almost immediately, while ReProver requires a warm-up period, possibly for building an internal context or search tree. The steady climb of ReProver suggests a more systematic, perhaps deeper, search process that pays off over time.

## Line Chart: pass@n-seconds ### Overview The chart visualizes the performance of two theorem-proving systems (COPRA and ReProver) with and without retrieval capabilities over wall-clock time. It measures the cumulative number of theorems proved as a function of elapsed time (in seconds), comparing four configurations: COPRA (GPT-4-turbo) with/without retrieval, and ReProver with/without retrieval. ### Components/Axes - **X-axis**: Wall-Clock Time in Seconds (n) - Range: 0 to 600 seconds - Labels: 0, 100, 200, 300, 400, 500, 600 - **Y-axis**: Number of Theorems Proved - Range: 0 to 70 - Labels: 0, 10, 20, ..., 70 - **Legend**: - **Orange**: COPRA (GPT-4-turbo) (with Retrieval) - **Blue**: ReProver (with Retrieval) - **Green**: COPRA (GPT-4) (without Retrieval) - **Red**: ReProver (without Retrieval) - **Legend Position**: Bottom-right corner ### Detailed Analysis 1. **COPRA (GPT-4-turbo) with Retrieval (Orange Line)** - Starts at ~5 theorems at 100s, rises steadily to ~70 theorems by 600s. - Slope: Consistent upward trend with minor plateaus. 2. **ReProver with Retrieval (Blue Line)** - Begins at ~10 theorems at 100s, increases to ~60 theorems by 600s. - Slope: Gradual rise with sharper acceleration after 300s. 3. **COPRA (GPT-4) without Retrieval (Green Line)** - Jumps from 0 to ~25 theorems at 100s, plateaus at ~60 theorems by 300s. - Slope: Sharp initial increase, then flat. 4. **ReProver without Retrieval (Red Line)** - Starts at 0, reaches ~20 theorems at 300s, ends at ~55 theorems at 600s. - Slope: Slow initial growth, accelerates after 300s. ### Key Observations - **Performance Hierarchy**: - COPRA (GPT-4-turbo) with retrieval outperforms all configurations, achieving ~70 theorems by 600s. - COPRA (GPT-4) without retrieval lags behind COPRA (GPT-4-turbo) but surpasses ReProver configurations. - ReProver with retrieval outperforms ReProver without retrieval but trails COPRA systems. - **Retrieval Impact**: - Retrieval significantly boosts performance for both systems. - COPRA (GPT-4-turbo) with retrieval gains ~15 theorems over its non-retrieval counterpart by 600s. - ReProver gains ~35 theorems with retrieval compared to without. - **Plateaus**: - COPRA (GPT-4) without retrieval plateaus at ~60 theorems after 300s. - ReProver without retrieval shows a slower but steady climb. ### Interpretation The data demonstrates that **retrieval mechanisms critically enhance theorem-proving efficiency**, particularly for COPRA (GPT-4-turbo), which achieves near-maximal performance (~70 theorems) with retrieval. The plateau in COPRA (GPT-4) without retrieval suggests inherent limitations in handling complex theorems without retrieval. ReProver, while less efficient overall, still benefits from retrieval, closing a ~35-theorem gap. The results imply that retrieval-augmented systems are essential for scaling theorem-proving capabilities, with COPRA (GPT-4-turbo) being the most effective configuration.