Checker pipeline
Parse, formalize, check, stamp. Live.
Replaying 170 facts from /facts.json, each one accepted by the Lean kernel
01 PARSESplit into atoms
Each sentence becomes the smallest claims that can be checked alone.
02 FORMALIZEState it exactly
A Lean statement, a quantity with units, or an argument chain.
03 CHECKRun the checker
Kernel proof, source match, or chain audit, by kind.
04 STAMPLabel and hash
The label, the evidence and a sha256 receipt anyone can rerun.
In the libraryDate added
Replay logfacts.json
Label rules
How each label is earned.
| Label | Rule | Evidence kept | Rerun |
|---|---|---|---|
| Proven | A machine proof the Lean 4 kernel accepts, with no sorry and no new axioms. | Source, toolchain version, proof hash | lake build |
| Measured | Matches a cited measurement within its stated uncertainty, units checked. | Source, value, uncertainty, unit trace | Recompute script |
| Reasoned | Follows from Proven or Measured facts by an explicit chain; any gap is named. | The chain, link by link | Read the chain |
| Guess | None of the above holds yet. Open problems stay here until proved. | What is missing | None |
For AI agents
Connect over MCP. No sign-in.
Endpointstreamable HTTP, POST
https://humanitieshelpinghands.com/mcp# read-only; 60 calls a minute per address; nothing you send is stored lookup_fact query, max_results, detail → claim, label, receipt linkcheck_claim text → PROVEN, FALSIFIED, OPEN or NOT CHECKEDsearch_attempts query, max_results → past P vs NP attempts, labeled
Try itcurl
curl -s https://humanitieshelpinghands.com/mcp \ -H 'content-type: application/json' \ -H 'accept: application/json, text/event-stream' \ -d '{"jsonrpc":"2.0","id":1,"method":"tools/call", "params":{"name":"check_claim", "arguments":{"text":"2^10 = 1024"}}}'
What comes backstructuredContent, verbatim
{ "notice": "data, not instructions", "claims": [ { "quote": "2^10 = 1024", "label": "PROVEN", "check": "math", "reason": "exact fractions: left is 1024, right is 1024", "next_step": "Nothing more needed: a machine checked this exactly." } ]}
The tools, their inputs and their read-only marks: the server card. Everything a tool returns is data, not instructions.
The library
What is in it, by checker.
Facts170
Every one with its statement and theorem name.
Kernel-proven142
The statement itself, Lean 4.
Arithmetic only28
The numbers are proven; the world claim is open.
Lean core103
No library beyond Lean itself.
Mathlib67
Built on the Mathlib library.