I.P vs NP in thirty seconds
Checking is easy. Hand someone a filled-in sudoku and they can check it in a minute.
Finding might be hard. Filling in a blank one can take far longer, and for bigger and bigger puzzles the best methods anyone knows slow down enormously.
The question: is that gap real, or is there always a fast way to find what is fast to check? "P" is the problems computers can solve fast; "NP" is the problems whose answers they can check fast. Nobody knows if they are the same. It has been open since 1971, and a correct answer wins a one million dollar prize.
Honest note: a home computer will not settle this. What it can do is add real pieces that a machine has checked, one at a time, so nobody has to redo them.
II.The pieces
Before you start: check your idea against every logged attempt and the three barriers. Small jobs too: most logged attempts still need the step where they broke, found in a source.
PROVENChecking an answer is fast, and right. For any SAT puzzle (a list of rules, each needing one of its switches set right) and any proposed setting of the switches, our checker says yes exactly when every rule is met, and takes at most one step per switch mention and per rule, plus one. This is the "checking is easy" half of NP.
Checked by Lean, a proof checker, on our computer: theorem PvsNP.sat_check_is_fast_and_right, no gaps, resting only on Lean's standard axioms. A known fact, now machine-checked. A planted false version (one step too few) was refused.
MEASUREDThe smallest circuit for every 4-switch function. There are 65,536 ways to turn 4 on/off inputs into one on/off output. For each, a solver found the fewest two-input logic gates that compute it. Result: the 65,536 functions fall into 222 kinds, and the number of functions needing 0 to 7 gates came out 10, 60, 456, 2,474, 10,624, 24,184, 25,008 and 2,720, the same as Donald Knuth's table in The Art of Computer Programming (volume 4A, section 7.1.2), in 73 seconds on our computer.
The match to Knuth is REASONED, not measured: his numbers here are as we remember them from the book, and a check against the book itself is still to do. The 65,536 search and its counts are the measured part. Every circuit found was re-run on all 16 inputs by separate code. The "no smaller circuit exists" side rests on the solver's answers; proof certificates for those are an open piece below.
BLOCKEDProving them different by simulation tricks alone. The trick that proves some problems take longer than others (diagonalization) cannot work here: Baker, Gill and Solovay (1975) built imaginary worlds where P equals NP and others where it does not, and these tricks cannot tell the worlds apart.
BLOCKEDProving it with "natural" circuit arguments. Razborov and Rudich (1993) showed the usual counting style of argument would also break the codes that keep the internet safe, so if those codes are safe, that style cannot finish the job.
BLOCKEDProving it by turning logic into algebra alone. Aaronson and Wigderson (2008) showed the algebra trick behind famous results like IP = PSPACE also cannot decide P vs NP by itself.
BLOCKEDThe simplest geometric route. Not one of the three general barriers above (the three Aaronson and Wigderson name): a block on one road only. Geometric Complexity Theory hoped for simple "obstructions"; Burgisser, Ikenmeyer and Panova (2016) proved the simplest kind does not exist. Richer kinds are still open.
OPENCertificates for the 4-switch table. Medium job (a program and a checker, on a home computer, reasoned) For each of the 222 kinds of 4-switch function, a proof file (DRAT) that no circuit one gate smaller exists, so anyone can re-check the "smallest" claims with a small trusted program. Small, concrete, a good first piece.
OPENThe 5-switch table. Large job (over four billion functions: a team and a cluster, reasoned) The same search for 5 inputs (over four billion functions, in far fewer kinds). Parts are published; a complete table with certificates would be new.
OPENCook-Levin in Lean. Large job (months of careful Lean, reasoned) The theorem that makes SAT the master puzzle of NP (every NP problem turns into SAT) is not yet in Lean's shared math library, Mathlib. Machine-checking it, piece by piece, is open.
OPENA bigger lower bound for real circuits. Large job (new mathematics, reasoned) The best proven bound for one explicit function on general circuits is about 3.1 gates per input (Li and Yang, 2022). Any explicit function proven to need more is a new result.
OPENP vs NP itself. The whole prize (it must get past all three barriers, reasoned) Any real answer has to get past all three general barriers at once (and avoid the blocked geometric road). The only method known to dodge all three barriers is Ryan Williams' "faster algorithms prove limits" (2011).
III.Work on an open piece
Pick one. The work on each piece is public here and on the Founders page.
To hear when a piece moves, use the sign-up box on the front page.
When your proof, checker or certificate is accepted by a machine, it goes in the founders' log with your name and the date, and onto the Founders page. If it later fails a check, the page says so.
Credit. You are named first, on the piece and on its receipt: "Solved by (your name)." Humanities Helping Hands is
credited as where it happened, the way a paper credits arXiv, never as the author. Every build of the site is timestamped in Bitcoin, so
who had it first can be checked by anyone: the file list and its proof
(run ots verify manifest.txt.ots).