Can you trust this paper?
· a first-pass review, with every answer labelled by what backs it
An AI wrote this maths paper, and a computer checked a formal version of its main theorem. Before trusting it, a reviewer still has to answer these questions by hand. Our agent answered them in seconds.
Still yours to judge: is the result new, and does it matter. The agent gives no verdict on the paper.
Review the paper with the copilot → one step at a time, with pictures, a chat, and code the agent runs for you
Review feed Supabase
Every finished review is stored as a row. Latest runs:
| row | paper | saved |
|---|
The evidence behind each answer (click to open):
Formal status
Statement versus claim human check needed
A proof checker confirms the right-hand side. Whether it says the same thing as the left-hand side is for a reader to judge.
Statement audit model-written, quotes verified
How far to trust the auditor measured
| seeded change to the Lean statement | kind | auditor raised a mismatch | verdict |
|---|
The model proposes flags; code keeps a flag only if both quotes occur verbatim in the paper and the Lean source. A flag is a prompt for a reader, not a finding.
Prior work search results, unreviewed
| found by search | year | in the paper's bibliography? |
|---|
Search via Monid (Exa), query built from the paper's own title and abstract. "Not cited" means the title is absent from the bibliography. The relevance call is the agent's (Agent37), made from each work's title and an excerpt of its text where the search returned one, not from the full work, so treat it as a lead to follow up.
Worked example
Recomputed here in exact rational arithmetic: distinct denominators, each at least 2, summing to the target.
Small cases recomputed: exhaustive search
| cups needed | first b that needs them | hardest fraction there | log log b |
|---|
This is the quantity the theorem bounds, computed exactly for small b. It illustrates the claim and does not test it: the theorem only speaks about b beyond an unstated threshold.
Proof map parsed from source
What does actually depend on?
Edges come from the paper's own cross-references. A result used without being cited by label would not appear.