WingNews logo WingNews
top | item 46583363

Show HN: The Thiele Machine – Coq-Verified Computational Model Beyond Turing

9 points| nwthiele | 1 month ago |github.com

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!

4 comments

order

nwthiele|1 month ago

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!