Hacker Newsnew | past | comments | ask | show | jobs | submitlogin
Show HN: The Thiele Machine – Coq-Verified Computational Model Beyond Turing (github.com/sethirus)
9 points by nwthiele 76 days ago | hide | past | favorite | 4 comments
The Thiele Machine is a formally verified universal computational model the surpasses Turing machines in key ways. It's fully proven in Coq (including kernel theorems and universality containment), features a python implementation for simulation and includes hardware designs in Verilog for potential FPGA/ASIC builds. The core idea: a paradigm shift using μ-bits for stricter computation under real-world constraints, tying into physics (e.g., Noether’s theorem) and emergence in chaotic systems.

The repo includes a 13-chapter thesis (PDF and sources), proofs, and tools for exploration. It’s aimed at formal methods enthusiasts, AI researchers, and hardware devs interested in verifiable, adaptive reasoning beyond traditional limits. Feedback welcome on the proofs, emergence chapter, or hardware impl, let’s collaborate!



Update: Thanks for the early feedback!

To clarify the “beyond Turing” claim without fluff—it’s not about hypercomputation magic, but introducing μ-bits as a constrained bit model that enforces physical realism (e.g., conservation laws via Noether’s theorem) in chaotic/emergent systems. This makes it “stricter” than TMs for certain real-world simulations, while still universal (proven in Coq, zero admits).

If you’re curious:

• Quick Python sim to play with: https://github.com/sethirus/The-Thiele-Machine/blob/main/sim... (try running a simple chaotic iteration).

• Hardware angle: Verilog for FPGA prototyping—anyone with ASIC experience want to collab on optimizing for low-power emergent logic?

• Thesis highlights: Ch. 7 on emergence in physics/AI, or Ch. 10 on why this could matter for verifiable ML training under constraints.

What breaks it for you? Proof holes, sim perf, or just the physics tie-in? Open to PRs or discussions!



> If you can't falsify it, you have to take it seriously.

No, I don't.


Fair, but the Coq proofs are zero-admit. Here is why it's falsifiable... https://github.com/sethirus/The-Thiele-Machine/blob/main/the... (Chapter 5)




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: