# Theorem Proving on PISA 2021-10-22 (test)

Source: [Theorem Proving on PISA 2021-10-22 (test)](<https://www.sota2.com/research/sota/theorem-proving-on-pisa-2021-10-22-test>)

Collection index: [llms.txt](<https://www.sota2.com/research/llms.txt>)

Data updated: 2026-02-26T06:04:57.054Z

Evaluation of model performance on theorem proving tasks using the test split of the PISA 2021-10-22 dataset, measured by Success rate (%).

A research result applies to its stated dataset, split, metric and evaluation configuration. Compare like-for-like settings, preserve the metric's unit and direction, and distinguish paper-reported results from independent reproduction. The best result recorded here is not a claim of exhaustive, current global coverage.

| Scope | Recorded value |
| --- | --- |
| Task | Theorem Proving |
| Dataset (including any stated split) | PISA 2021-10-22 (test) |
| Metric | Success Rate |
| Unit | PERCENT |
| Direction | Higher is better |
| Results loaded | 5 of 5 |
| Coverage | All results currently returned for this benchmark |

Evaluation settings may differ between results. The original papers and recorded configurations are needed to establish comparability. A shared metric name alone does not establish an identical protocol.

## Metrics

- [Success Rate](<https://www.sota2.com/research/sota/theorem-proving-on-pisa-2021-10-22-test.md?metric=Success%20Rate>): Higher is better; unit: PERCENT.

## Recorded results

| Method | Success Rate | Result date | Report paper |
| --- | --- | --- | --- |
| Thor | 57 | Not recorded | 68fa6c981e209131cea34bc6 |
| Language model ∪ Sledgehammer | 48.8 | Not recorded | 68fa6c981e209131cea34bc6 |
| Language model | 39 | Not recorded | 68fa6c981e209131cea34bc6 |
| LISA | 33.2 | Not recorded | 68fa6c981e209131cea34bc6 |
| Sledgehammer | 25.7 | Not recorded | 68fa6c981e209131cea34bc6 |

### Thor

Success Rate: 57. Result ID: 698f23433a6c314849f61fe8.

[Reporting paper](<https://www.sota2.com/research/paper/68fa6c981e209131cea34bc6.md>)

[Method origin paper](<https://www.sota2.com/research/paper/68fa6c981e209131cea34bc6.md>)

Recorded evaluation configuration: Not recorded. This record does not assert independent reproduction.

### Language model ∪ Sledgehammer

Success Rate: 48.8. Result ID: 698f23433a6c314849f61fe7.

[Reporting paper](<https://www.sota2.com/research/paper/68fa6c981e209131cea34bc6.md>)

Recorded evaluation configuration: Not recorded. This record does not assert independent reproduction.

### Language model

Success Rate: 39. Result ID: 698f23433a6c314849f61fe6.

[Reporting paper](<https://www.sota2.com/research/paper/68fa6c981e209131cea34bc6.md>)

Recorded evaluation configuration: {"parameters":"700M","sampling temperature":1.2,"search strategy":"best-first search"}. This record does not assert independent reproduction.

### LISA

Success Rate: 33.2. Result ID: 698f23433a6c314849f61fe4.

[Reporting paper](<https://www.sota2.com/research/paper/68fa6c981e209131cea34bc6.md>)

Recorded evaluation configuration: Not recorded. This record does not assert independent reproduction.

### Sledgehammer

Success Rate: 25.7. Result ID: 698f23433a6c314849f61fe5.

[Reporting paper](<https://www.sota2.com/research/paper/68fa6c981e209131cea34bc6.md>)

Recorded evaluation configuration: {"timeout limit":"30s","ATPs":"E, SPASS, Vampire, Z3, CVC4"}. This record does not assert independent reproduction.

Page 1 of 1. This is an index page, not the full collection.