Acorn's standard library of mathematical facts.
This repository is a mathematics library, written in Acorn, building up mathematics from the inherent axioms. The implementation of the Acorn language itself, the integrated AI, and the VS Code extension are handled in the acorn repository. The code for the acornprover.org website, including documentation, is in the acornprover.org repository.
We welcome both human and AI contributions. The goal of acornlib is to be a repository of all known mathematics. So you're welcome to contribute anything that isn't in here yet.
If you have OpenAI Codex and you'd like to use it to contribute, the first step is think of a project you'd like to contribute. A theorem you'd like to prove, or an area of mathematics you'd like to generally formalize. Then ask Codex to do it, with the work-on-project skill.
If you're looking for ideas, jump into Discord and we're happy to discuss.