How to Contribute

Contributions of all kinds are welcome — from adding new formalisations to fixing inaccuracies.

Ways to contribute

  1. Add new problem formalisations. We encourage adding formalisations of open conjectures from:
  2. Open issues describing problems you'd like to see formalised. Include links to references and a precise informal statement.
  3. Formalise a proposed problem. Browse unassigned new conjectures or good first issues and comment to claim one.
  4. Improve tagging and referencing — add missing @[AMS] tags or source links to existing files.
  5. Fix misformalisations. PRs fixing incorrect formal statements are especially appreciated.

Contribution process

  1. Sign the Google CLA (required once per contributor).
  2. Open a GitHub issue describing your planned contribution.
  3. Fork the repository and create a branch.
  4. Add your formalised conjecture(s) in the appropriate directory.
  5. Ensure the project builds: lake build.
  6. Submit a Pull Request.

File structure conventions

Every .lean file should follow this structure: 

/-
Copyright YYYY The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 …
-/

import FormalConjectures.Util.ProblemImports

/-!
# Problem Title
*Reference:* [source](https://…)
-/

namespace MyProblem

@[category research open, AMS 11]
theorem my_conjecture : Statement := by
  sorry

end MyProblem

The @[category] attribute

Every statement must have exactly one category tag:

  • @[category research open] — unsolved open problem
  • @[category research solved] — informally or formally solved
  • @[category research formally solved using lean4 at "url"] — has a formal Lean 4 proof
  • @[category graduate] / undergraduate / high_school]
  • @[category test] / API] — internal use

The @[AMS] attribute

Every statement must have at least one AMS MSC2020 subject tag. Use #AMS in VS Code to list all valid values. 

@[AMS 11]       -- Number Theory
@[AMS 5 11]     -- Combinatorics + Number Theory

Style guidelines

  • One problem per file (variants and special cases may share a file).
  • Include a reference comment linking to the source of the conjecture.
  • Use theorem or lemma for problem statements.
  • For questions ("Does P hold?"), use the answer(sorry) elaborator.
  • Bespoke definitions are fine; add basic API tests for them.
  • Follow the same AI usage conventions as Mathlib.

Getting started with Lean 4

If you're new to Lean 4, install elan, lake, and Lean, then: 

git clone https://github.com/google-deepmind/formal-conjectures
cd formal-conjectures
lake exe cache get   # download prebuilt Mathlib oleans
lake build

Join the Formal Conjectures Zulip channel for help and discussion.