The system performs expert iteration over large Lean datasets and uses a critic to prioritize easier problems and guide deeper proof searches.
InternLM2.5-StepProver reported 65.9% on miniF2F-test and proved or disproved 17.0% of Lean-Workbook-Plus problems.
It provided an open empirical example of theorem-proving performance scaling with data, search and compute.
Significance rationale: StepProver showed how large problem banks and compute-intensive expert iteration can steadily raise open formal theorem-proving performance.
—
—
The Chronicle records this event from the cited primary or official source; the status does not imply independent Chronicle verification.
This corpus refresh added a directly inspectable public artifact maintained by the authors or releasing organization. E3 records artifact-level inspectability and does not imply independent verification of the underlying scientific or mathematical claim.
No corrections recorded.
