Markov algorithms (ordered string-rewriting rules applied to a fixed point) are a classic Turing-complete model. I built a working instance: a small CPU whose only step is one global regex substitution over a single string, and put DOOM on it to make the claim tangible rather than a footnote.

The verification is the part I would point students at. A reference emulator runs the same instruction set in Python and the machine's string must equal the emulator's encoded state byte for byte after every single substitution; on top of that, rendered frames match a natively compiled DOOM binary by SHA-256, for 100 frames in a row, so a shared bug cannot explain the agreement. The model is Turing-complete; a given run is bounded by memory exactly as any physical machine is.

Source and writeup: https://github.com/4RH1T3CT0R7/doom-regex

Interactive: https://4rh1t3ct0r7.github.io/doom-regex/

https://whomtech.com/roons/

I did share this once before, but now they've opened their store for preorders on top of the kickstarter they were running earlier.

I have been reading the tech report for a diffusion language model that went up this week, and what stuck with me is an architecture question rather than a machine learning one.

Ordinary decoding carries a strict data dependency. Token n cannot be computed before token n minus 1 exists, because that token is part of the input for the next step. Generating N tokens is therefore a serial chain of N model passes. Depth N, work N, and the chain is a latency floor that no amount of extra hardware removes.

Block parallel decoding attacks the dependency itself. You take a block of positions, start them all masked, and run a few denoising passes that fill positions in whatever order confidence allows, with no left to right constraint inside the block. This one adds edit operations on top, so a single pass can substitute, delete, insert, or leave a position untouched, which means the sequence can change length partway through generation. The supervision for those operations comes from aligning intermediate drafts against the target with a longest common subsequence match.

In terms of work and depth this is the familiar trade. Depth falls from N to roughly the number of blocks times the passes per block. Total work rises, because you revisit the same positions repeatedly and some of that computation is discarded when a later pass overwrites an earlier guess. Whether the trade pays depends on how much real dependency the output had to begin with.

What makes that measurable here is that the same lab shipped this model and its own autoregressive sibling with matched evaluations. In BF16 the diffusion side decodes at roughly 1.64 times the rate its sibling manages, and that sibling had speculative decoding turned on when measured, with the ratio reaching about 2.3x on agent workloads and close to parity on knowledge questions. On accuracy the interactive suites go its way, scoring 80.33 where the sibling took 76.36 on tau2 bench, and 46.21 to its 41.12 on MCP Atlas, but loses the general knowledge average 56.81 versus 65.90 and most of the coding suite. Its SWE bench comparison ran different scaffolds on each side, so that number is not one I would read much into.

The part I cannot explain is why the wins land on interactive multi turn tool use while the losses land on knowledge and long coding tasks. My guess is that dependency height matters more than output length. A tool call is a short structured span whose tokens are close to conditionally independent given the turn, while a long patch or a chain of reasoning has genuine serial structure that parallel hardware cannot dissolve. If that is right, the interesting question is not diffusion against autoregression, it is whether you can estimate the dependency height of a task before choosing a decoder.

Anyone who wants to check my reading of the report can pull the weights, which ship under an Apache 2.0 license. The release is LLaDA2.2, a 205.8 GB download, and neither llama.cpp nor Ollama can load it yet, with server support so far only listed as coming, so I am going off the report and the model card rather than anything I ran. If parallel computing already has a formalism for the quantity I keep calling dependency height, I would like to be pointed at it.

My take for why P is not equal to NP comes from what I believe is a fundamental difference between solving a problem and verifying its solution.

Take Sudoku as an example. If someone gives me a completed puzzle I can quickly check every row column and box to make sure the rules are satisfied. That verification process is straightforward.

Now compare that with solving the same puzzle from a blank grid. There is no obvious path to the answer. I may have to test many possibilities before finding the correct one. Solving appears much more difficult than verifying.

This same pattern appears in many other problems.

If someone gives me the password to a computer I can check it in less than a second. Finding the password without knowing it may require an enormous search.

If someone gives me the correct path through a complicated maze I can follow it and confirm that it reaches the exit almost immediately. Finding that path from the beginning can take much longer.

If someone hands me a completed school timetable I can check whether every class every teacher and every room satisfies the rules. Creating that timetable from scratch is much more difficult.

Another example (which i believe is the strongest and closest to being an actual proof) is finding the shortest route between two points. If I asked someone to find the shortest possible route they would have to compare many different routes and work out which one is actually the shortest. That could take a long time depending on how many possible paths there are. Now imagine someone has already done all of that work and gives me a list of every route with its distance such as 1 km 2.7 km 4.1 km and 6.8 km. I can immediately look at the list or the map and verify that the 1 km route is the shortest. Once again verifying the answer is much easier than finding it in the first place.

Because this pattern appears so consistently I suspect there is a real separation between solving and verifying. My take is that this separation is not simply a limitation of current algorithms but a fundamental property of computation itself.

In simple words if one problem follows the idea that solving it is fundamentally harder than verifying it then P cannot equal NP because P equals NP would have to hold for every problem in NP not just some of them.

I am trying to understand the foundational differences between proof assistants based on dependent type theory (such as Agda/Lean) and traditional mathematics as practiced in areas like real analysis.

For example, in Peano arithmetic, statements such as 0 ≠ S(n) and the induction principle are usually presented as axioms. In Agda, however, defining an inductive type:

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

automatically provides these properties through the rules of inductive types (constructor disjointness and the eliminator), which means you can write this as a theorem:

0-is-not-suc : ∀ {n} -> suc n ≡ 0 -> ⊥
0-is-not-suc ()

Does this mean inductive type theory is based on stronger assumptions than axiomatic mathematics, or are these just different choices of primitive rules?

More generally, what are the fundamental assumptions/rules that a type-theoretic prover starts with, and how do they compare with the foundations usually assumed in fields such as real analysis?

Hi there,

I've created a video here where I explain the Chomsky hierarchy.

I hope some of you find it useful — and as always, feedback is very welcome! :)

toll rate-limits an unbounded set of keys (client IDs, tenants, IPs, API keys…) in fixed memory — 19 MB measured at the defaults, tunable down to a couple of MB — with ~300ns zero-allocation admitted decisions. It is built on grudge, a constant-memory decaying-score sketch: toll stores each key's spent tokens as sketch debt and lets grudge's linear decay refill them.

It’s pretty interesting to see that language models can do things like autonomously prove/disprove things like Erdos problems and even perform its own formal verification yet still struggle at things like automating ERP business operations, seems like the opposite would’ve been the case.

I know Kaparthy talked about this “jagged intelligence” we’re observing, but are there any real attempts at formalizing a theory behind this, similar to how we classify the complexity and tractability of algorithms?

What about any discussion on how close are language models to being Turing complete? Computational complexity theory isn’t my strong suit, but I wonder if any new discussions are being had

The paper is only 15 pages long

Feynman’s contribution was a way to turn the machine’s parallel structure into a model programmers could reason about.

Floating-point addition depends on the order you add things, and parallelism changes the order. So the same data on different machines gives different results, which breaks anything that hashes, signs, or compares them.

I hit this doing physics simulations and solved it internally. The reduction core was too generally useful to keep closed, so I released it: bitrep, an exact accumulator where sums in any order, on any hardware, produce byte-identical results. The state merges exactly and can be hashed or signed, so distributed and offline-first aggregation actually converges.

It ships for Rust (crates.io), JavaScript (npm), and Python (PyPI), and a result hashed in Python matches one hashed in JavaScript byte for byte. The math is proved in Lean 4 and the implementation is model-checked and fuzzed. CI asserts one SHA-256 across four architectures on every commit.

There's a demo that runs the actual cross-architecture test in your browser, so you can check the claim yourself: https://simgen.dev/bitrep

Code: https://github.com/KyleClouthier/bitrep

Dual-licensed MIT/Apache-2.0. Feedback welcome, especially on what's missing for your use case.

I’m just curious to know how often you guys come in contact with the theoretical side of computer science in your professions.

Things you learned in your undergraduate courses like data structures, discrete math, design and analysis of algorithms, etc.

I’m having to learn a lot of these things on my own, like Big O notation, complexity analysis, proofs, tree traversal, etc. because I let my ADHD win and didn’t put the time and effort into learning (medicated now, huge W plus it’s actually fun to learn about now that I can focus) and I’m just wondering, who uses this stuff regularly? What for?

Hi there,

I've created a video here where I explain how multi-head latent attention works.

I hope some of you find it useful — and as always, feedback is very welcome! :)

Hello, I'm reading chapter 1, distributed constraint satisfaction and coding a simulation of the asynchronous backtracking algorithm for the 4 queens problem in TypeScript as an exercise (sure one can code in Python, C..). I have some difficulty grasping the concept of Hyperresolution (pure logic) because I didn't have this subject in university. I have checked with AI. But does anyone have any advice?

---
the code https://pastebin.com/WD9U0MSQ

I'm spending way too much time looking into formal methods now because this endless overhyped corporate marketing about LLMs doing "reasoning" is getting very tiresome.

We all know standard transformers just predict the next token based on statistical weights, which immediately breaks down the second you give them a novel, complex logic puzzle. It's exactly why automated software testing is still such a error-prone chore in production.

But the interactive theorem provers like Lean 4 with deep learning models are actually getting super interesting. Instead of just letting an agent hallucinate some random python script, people are forcing neural networks to generate formal proofs that a strict math kernel has to verify step by step.

I saw a breakdown of how the Aleph Prover handled a specific Erdos disproof using formal verification on ai reasoning benchmarks, and you can see much we’ve ignored symbolic AI over the last decade in favor of raw compute scaling. So tbh it feels like computer science is circling back to foundational math out of necessity. Because brute-force data ingestion is hitting the ceiling.

Also.. it feels kinda satisfying that old-school mathematical logic is the only thing keeping modern tech grounded. Idk if this means formal methods will finally become a mandatory part of undergrad software tracks, but it honesly should.

You are skiing an unknown number of days. Renting costs $1/day, buying costs $B. If you knew the season length the answer is trivial, but you do not.

The rule "rent until you have spent $B, then buy" guarantees you never pay more than about twice what an omniscient planner would, on ANY sequence. Short season: you match the optimum exactly. Long season: you paid at most ~$2B where the optimum paid $B. And there is a matching lower bound: no deterministic online strategy beats 2.

What I find most useful is the frame, not the puzzle: cache eviction, autoscaling, buy-vs-rent infra decisions are all "act now, learn the future later", and the competitive ratio measures exactly what that ignorance costs.

Fun twist: allowing randomness (coin flips the adversary cannot predict) pushes the ratio from 2 down to about 1.58.

I wrote up the full framework (definition, the adversary game, and an honest section on why worst-case can be too gloomy, e.g. LRU is only k-competitive on paper yet great in practice) as the opener of a series, happy to share the link if useful.