User:GregoryMorse
I am Gregory Morse, originally from Los Angeles, USA, and a PhD candidate and lecturer in the Department of Programming Languages and Compilers at Eötvös Loránd University (ELTE), Budapest, Hungary. My interests include algorithms, decompilation, self-modifying code, control-flow graphs and formal verification.
Contributions
Guides
- Computability and provability guide — computability, provability, BB/BBB, the halting problem and logical independence.
Beeping machines
Two-symbol, blank-tape beeping machines using a designated beep state, developed with Claude assistance. I completed the suite's Lean formalizations on 9 November 2026.
| Problem | States | Proof |
|---|---|---|
| P = NP | 278 | Lean proof; NP-completeness proof |
| P = PSPACE | 291 | Lean proof |
| P = PP | 295 | Lean proof |
| NP = coNP | 317 | Lean proof |
| Integer factorization in P | 324 | Lean proof |
| Discrete logarithms modulo primes in P | 400 | Lean proof |
| Linear-time multiplication | 403 | Lean proof (queue-of-stacks model) |
| Graph isomorphism in P | 415 | Lean proof |
| Linear-size NTT circuits | 469 | Lean proof (assuming PrimeEx)
|
| Twin prime conjecture | 19 | Lean proof; quasihalts iff the conjecture is false. |
The linked proofs state the precise language and machine-model formulations.
Wiki contributions
- Machine and formalization entries in TMBR: November 2026 and Cryptids.
- Clarification of beep-state and beep-transition conventions in Beeping Busy Beaver.