User:GregoryMorse: Difference between revisions
Jump to navigation
Jump to search
GregoryMorse (talk | contribs) Created page with "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, provabi..." |
GregoryMorse (talk | contribs) Unconditional NTT |
||
| Line 46: | Line 46: | ||
| Linear-size NTT circuits | | Linear-size NTT circuits | ||
| 469 | | 469 | ||
| [https://github.com/GregoryMorse/NP-complete/blob/main/formal/ZP/MainNTT.lean Lean proof] | | [https://github.com/GregoryMorse/NP-complete/blob/main/formal/ZP/MainNTT.lean Lean proof] | ||
|- | |- | ||
| Twin prime conjecture | | Twin prime conjecture | ||
Latest revision as of 10:52, 10 November 2026
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 |
| 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.