Misleading formalizations of P vs NP — a spot-the-flaw challenge set

This is a set of nineteen AI-generated Lean 4 / mathlib formalizations of P versus NP. While some are correct formalizations, others are deliberate misformalizations: they look right, but a flaw somewhere makes P = NP or P ≠ NP provable without solving the actual P vs NP problem, or makes a genuine proof impossible.

Instructions for humans

Your task, for each challenge, is to decide whether it is faithful or a misformalization, and in the latter case to find the concrete flaw.

Each challenge N consists of a file Challenges/Challenge_N.lean, which imports only Mathlib, and one or two .json configs next to it for lake comparator (see below). The challenges are independent of each other, so you can do them in any order, or only do a few (or even one) of them. Be aware, though, that several of them reuse the same kind of machine model under different names, so a reveal about one model may help you with another challenge.

To browse the files in an editor with Mathlib available, first run lake exe cache get in this directory.

You are supposed to solve this without the help of AI tools.

You do not need to write lean code. Provide solution modules is not the task.

Modes and comparator config files

Each challenge is in one of two modes.

Challenge mode. The main sorried theorem states the open problem, either P_ne_NP : P ≠ NP or P_eq_NP : P = NP, and there is one config, Challenge_N.json.

Conjecture mode. The file defines MainConjecture : Prop and has two sorried main theorems, conjecture_solution : MainConjecture and conjecture_refutation : ¬MainConjecture. There is one config per side, Challenge_N_proof.json and Challenge_N_disproof.json, and a solution only needs to solve one of them.

In both modes, a file may also contain further sorried sanity-check lemmas, such as P_subset_NP : P ⊆ NP. These are believed to be provable; a config that lists one under theorem_names forces a solution to prove it as well, which rules out some degenerate definitions.

Each .json file is a config for lake comparator, which checks a solution module against the challenge module. A solution module restates the challenge module and proves the theorems listed under theorem_names without sorry, using no axioms beyond those listed under permitted_axioms. lake comparator would then check that every constant reachable from those theorems is the same in the solution as in the challenge. The only exceptions are the constants listed under definition_names, called "definition holes": the solution may give them any body it likes, as long as the type matches. Anything that is not reachable from a listed theorem is never inspected.

You don't need to run lake comparator to play, but you do need these semantics to judge some of the challenges. The .json files are part of the challenge: whether they list everything that the .lean file sorries is part of what you are judging.

How the challenges were created

I tasked Claude Fable (5.1) to create several misleading or faithful formalizations of the P vs NP problem, with the misleading formalizations designed to fool a human without AI help.

For each challenge, an independent biased coin flip was performed: the challenge had to be faithful with probability 38% and misleading with 62%.

Things that would count as misformalization:

• it enables a much easier proof of P = NP or P ≠ NP;
• it makes a genuine proof impossible;
• it states something other than P vs NP;
• a definition hole admits an unintended instantiation;
• its .json config is wrong, for example because it omits a sorried lemma or confuses definition holes with theorems.

Faithful formalizations may contain smaller red herrings, too. Variety among the formalizations was explicitly welcome. Any standard way of stating P vs NP counts as faithful, for example a different machine model, SAT ∉ P in place of P ≠ NP, or NP ⊆ P in place of P = NP. An unusual frame is not a flaw by itself.

Reveal files

The answer to each challenge is in its own reveal file, reveals/reveal_N.md.scrambled. The reveal files are XOR-scrambled so that you don't spoil a challenge by accident. This is obfuscation, not encryption; the key is in scramble.py.

python3 unscramble.py reveals/reveal_3.md.scrambled   # one answer
python3 unscramble.py reveals/*.scrambled             # everything

Each reveal explains the challenge's deliberate flaw(s), if it has one. It also explains why each of the other sorried sanity-check lemmas is believed to be provable.

reveals/lean_notes/ is not scrambled and contains spoilers.
These files contain Lean code that may be referenced in the reveal files. The filenames are random, and not every file is referenced by a reveal, so the directory listing tells you nothing on its own. Opening a file can spoil a challenge. Not all flaws or exploits mentioned in the reveal files are backed by Lean code. Each file imports only Mathlib, so you can check it with lake env lean <file> from this directory (after fetching Mathlib with lake exe cache get).