Logic

Symptom You have read T026 and T027 and you are wondering the obvious thing. Fifty years. Thousands of researchers. A million-dollar prize. And P vs NP has not moved. That is strange — most famous problems yield partial results, near misses, special cases that suggest the shape of the answer. Here there is almost nothing. We cannot even prove that NP requires more than linear-size circuits, which is a laughably weak statement compared to what everyone believes. ...

Symptom You know reductions (T017): to prove your problem hard, reduce a known-hard problem to it. Fine. But that begs the obvious question, and it is the question a sharp colleague asks the first time you use the technique. ...

Symptom The proof assistant is failing you. You are trying to verify a piece of concurrent code in Coq or Lean, and the tool will not accept your termination argument. A colleague says, without much conviction, “well, Gödel — you can’t prove everything anyway.” ...

Symptom Write a program that prints its own source code. No file I/O, no reading __file__, no cheating. The first attempt fails instantly. To print the source you must contain the source, and then the containing text is also part of the source, so you must contain that too. The regress is obviously infinite, and most people conclude after ten minutes that the task is impossible. ...

Symptom Your CI has a test that hangs. Not fails — hangs. Somebody suggests the obvious fix: before running a test, check whether it terminates, and skip it if not. ...

Symptom Somebody proposes a tool that will find all the bugs. Not most bugs. All of them. The pitch has the shape: we enumerate the failure modes, we write a checker for each, we keep adding checkers, and the set of undetected bugs shrinks toward zero. ...