# formal-math-autoformalization by Agentic Commons: Dataset
Source: https://savrn.com/datasets/formal-math-autoformalization
Markdown alternate of the page above; the site index is https://savrn.com/llms.txt

---

## Dataset Card

By Agentic Commons, published under cc0-1.0, revision 8727865c629e.

### Formal Math Autoformalization Dataset

A growing, CC0 public-domain corpus of ⟨natural-language statement ↔ Lean 4 statement + proof⟩ pairs, contributed through the Agentic Commons network.

Why this is scarce data. Mathlib already contains millions of proven Lean theorems — but as bare Lean, with no paired natural language:

```
theorem add_comm (a b : ℕ) : a + b = b + a := ...   -- no "addition on naturals is commutative" attached
```

The scarce, valuable artifact is the pairing of the human-language statement with a Lean formalization — especially statements not already in Mathlib. Mathlib gives you the Lean half (the answer); this dataset supplies the missing human-language half and ties the two together, with a machine proof that the Lean half is actually a theorem.

- Lean toolchain: leanprover/lean4:v4.30.0
- Mathlib revision: c5ea00351c28e24afc9f0f84379aa41082b1188f
- License: CC0-1.0 (public domain)

### What's in it / intended use

[Read the full dataset card (761 words)](https://savrn.com/datasets/formal-math-autoformalization/card)

## Structure

### default 3,623 rows

| Split | Rows | Size |
| --- | --- | --- |
| train | 3,623 | 2.6 MB |

submission_markerstringacg_urlstringcontributor_handlestringnl_statementstringlean4_statementstringlean4_proofstringverification_levelstringaxioms_usedlistmathlib_conceptslistmathlib_revisionstringlean_toolchainstringlicensestringprovenancestringbacktranslationstringnli_scorefloat64difficulty_tierstring

## Details

Repository

AgenticCommons/formal-math-autoformalization

Publisher

Agentic Commons

Task category

Text generation

Tags

lean4, mathlib, autoformalization

Size category

n<1K

Languages

en

Revision

8727865c629ece21dd609d34d44fb93016d24fbf

Last updated

2026-09-21

## Files

3 files, 3.2 MB in total.

Data1 file · 3.2 MB

Documentation1 file · 6.3 KB

Repository1 file · 2.5 KB

Every file

| File | Type | Size | SHA-256 |
| --- | --- | --- | --- |
| data/formal_math.jsonl | Data | 3.2 MB | — |
| README.md | Documentation | 6.3 KB | — |
| .gitattributes | Repository | 2.5 KB | — |

## License and Download

License

cc0-1.0

Access

No access gate

[Download from Agentic Commons](https://huggingface.co/datasets/AgenticCommons/formal-math-autoformalization)

Released by Agentic Commons through its official repository on Hugging Face. [Read the license](https://creativecommons.org/publicdomain/zero/1.0/).

## Agentic Commons

[All models and datasets](https://savrn.com/model-publishers/agenticcommons)

## Explore More

- [The dataset directory](https://savrn.com/datasets)
- [The model directory](https://savrn.com/models)
- [Research papers](https://savrn.com/papers)

## Source

- Repository metadata, read 2026-10-23.
- [Hugging Face record](https://huggingface.co/datasets/AgenticCommons/formal-math-autoformalization)
- [How the hub is built](https://savrn.com/model-hub/methodology)