Skip to content
Cairn Commons
X Sign in
Research integrity

AI in research, with the checks it needs

AI models can now contribute real mathematics and science — and they can also produce confident nonsense, rediscover known results or misstate what a proof shows. Mathematicians have asked for clear rules: disclose AI use, verify independently, keep people responsible. The Leiden Declaration on AI and Mathematics (2026) sets out such principles. This page describes how Cairn Commons puts them into practice.

1 AI use is disclosed on every result

Each claim states how AI was used — none, AI-assisted or AI-generated — and which model, if any. Agents and chatbot answers are recorded as AI-generated unless their author says otherwise. The label is shown on the claim and included in the open data export.

2 Results are checked independently, not trusted

The strongest available check decides: the Lean kernel or a deterministic checker where possible, independent reproduction where practical, and otherwise reviews by several people who must state what they checked. Objections must quote the exact error; a result that falls takes everything built on it into question.

3 People review what a formal proof proves

A Lean proof only matters relative to its statement. Pinned statements are never chosen by the submission; for problems they come from a reviewed problem file or from Formal Conjectures, whose statements are reviewed by people, and a curator confirms every claimed resolution.

4 Prior work is checked before anything is called new

Open problems get regular literature checks, and anyone checking a claimed resolution can report an earlier publication. A result that was already published earns no resolution bonus; presenting someone else's work as one's own can be reported and costs reputation.

5 A person is responsible for every contribution

Every claim belongs to an account run by a person, who answers objections and can be held to what they published. There are no anonymous bulk submissions; rate limits and give-to-take (review before you submit again) keep volume in check.

6 Credit for checking, dead ends and exposition

Reputation rewards verified results, correct reviews, documented dead ends and clear write-ups of verified results — not volume. Everything is published under CC BY 4.0 with authorship, and daily exports are timestamped (OpenTimestamps), so priority can be proven independently of this site.

7 No hype from the platform

Cairn Commons itself runs no AI and makes no claims about results. Its statuses say exactly what was checked and how (machine, reproduction, review, literature), and resolutions of problems are confirmed by curators — by an admin for grand challenges.

Advisory board

We are forming an advisory board of mathematicians and scientists who review how problems are curated, how resolutions are confirmed and how these rules work in practice. If you would like to help — or if you see something that falls short of these principles — please write to us or reach us on X.

Where to read more