Research results

§Tables: when the key can be the address

At one million integer IDs, the direct-coordinate table in hashtrinity looked up a value 2.2× faster than hashbrown, using 27% less memory.

The idea is simple. If the keys are IDs in a known range, the ID can tell us where the value lives. We can skip hashing it and searching for a slot.

The advantage changes with the workload. At four million IDs, random lookup took 13.3 vs 14.3 ns. Once fetching memory dominates, saving the hash matters much less.

String keys need a different table. At four million opaque keys, the exact table took 30.3 vs 35.2 ns for successful lookups. Missing-key lookups favoured hashbrown: 34.2 vs 11.8 ns.

These are the July 2026 results from hashtrinity, the table library being carried into Apeiron. The full comparison covers the other workloads and parallel baselines: i9-14900KF, 64 GiB RAM, release builds, 15–35 observations per cell.

§Apeiron: CPU inference versus llama.cpp

On Qwen3.5-0.8B Q8_0, Apeiron reached 2.45× llama.cpp's prompt-processing speed in the 512-token test. Generating tokens reached 1.76× in the separate 200-token benchmark run. Both ran on the same i9-14900KF, entirely on CPU.

These runs were recorded on 30 September 2026 UTC. The raw measurements identify the measured revisions and workloads.

There are two jobs here. First the model reads the prompt, usually called prefill. Then it generates tokens, usually called decode. Improving one doesn't automatically improve the other.

Reading the prompt

512 tokens · tokens/s

Apeiron1,188.65

llama.cpp453.90

Generating tokens

64 steps · tokens/s · 200-token benchmark run

Apeiron88.99

llama.cpp50.38

The two runs give the following measurements. Each generation test starts from a fresh state; it runs separately from prompt processing.

The work behind these numbers is in the merged runtime. The measurements were recorded on 30 September 2026 UTC. The raw rounds and calculated medians include the model and build identities.

How the CPU comparison was measured

Both engines load the same Q8_0 model file. Apeiron uses its floating-point carrier and Q8 activation kernels. Each workload is warmed before measurement, with five interleaved rounds and a host-busy threshold below 5%. llama.cpp is tested at 8, 16, 24 and 32 threads; each task uses its fastest thread count in that round. Apeiron keeps roughly 24 CPU cores busy. These are throughput measurements with independently tuned execution.

Prompt lengths match. Apeiron reads recorded prompt IDs; llama-bench uses synthetic IDs. The 64-step decode tests start from position zero, independently of prefill. The comparison measures throughput rather than identical generated text. Model loading is outside the timers. Speed ratios are medians of the five paired ratios, so dividing the two displayed medians can give a slightly different number.

The measured Apeiron revision is 04d2060; llama.cpp is 0324696b8. The runtime was subsequently merged at 01de89d. Later changes need their own measurements.

§A later decoding experiment

A separate experiment tries several likely next tokens together, then keeps the ones the model accepts. On a code prompt it reached 110.76 tokens/s, against 51.02 for llama.cpp's ordinary greedy decoder: a 2.14× paired speed ratio. On a prose prompt, the ratio was 1.80×.

This probe uses the same 200-token prompt on both engines. Its speculative path produces the same 64 tokens as Apeiron's own greedy path. On the code example, Apeiron and llama.cpp produce different continuations; on the prose example, all 64 tokens match. The experiment record and five raw rounds give the comparisons. This is a separate decoding experiment, with integration and longer quality comparisons ahead.

§Song: from the operation to its bytes

Multiply the pairs (2, 3) and (5, 7) on the hyperbolic face. The answer is (31, 29): the first slot is 2 × 5 + 3 × 7; the second is 2 × 7 + 3 × 5.

Gen3 follows that multiplication all the way to the bytes the processor executes. The proof covers every combination of the four 64-bit inputs, including arithmetic wrapping at 64 bits. It also shows that the operation leaves data memory unchanged.

This matters because checking the formula alone leaves the implementation to trust. Here the argument includes the generated instructions and their encoding. The full compiler and kernel are ahead.

The native proof and byte image

The proof checks execution against Song's x86-64 model, from its defined entry state through the return. The instruction generator, word arithmetic and 32-byte image are available together. Hardware correspondence and the C calling convention remain assumptions supported by tests.

§The earlier compiler was quick

On 100 small arithmetic functions, the gen2 compiler produced an executable in 5.8 ms. Clang took 52.6 ms, GCC 135.5 ms, and Rust 47.8 ms. Those are median compile-and-link times over seven interleaved samples on 4 October 2026.

It's a useful result for the wait between changing a programme and running it. The compilers do different optimisation and linking work; this arithmetic workload has no proof contracts. The method, samples and sources in C, Rust and Slang give the comparison.

§Keep the proof checker small

The useful finding was that a small, sound kernel was already there. In the gen1 tree, that kernel written in Lean occupied 706 lines, alongside a 34,502-line Slang prover. We had a much smaller piece to build on.

Finding a proof and checking it are different jobs. Finding one can involve a lot of search, failed attempts and clever machinery. Checking the result should depend on a small set of rules. That lets us improve how we find proofs while keeping the rules for accepting them steady.

That's the direction gen3 takes. I want to spend the work on carrying the argument through the compiler to the machine. The native multiplication shows the first concrete step: the proof reaches the instructions and their bytes.

The code-size and maintenance record

The gen1 Slang prover occupied 34,502 lines; the specific sound kernel module written in Lean occupied 706. The ratio was about 49 to one. This compares those two components, rather than the prover with the whole Lean proof library. The kernel size record gives the source.

The newer history census counted 162,126 changed lines, of which 97,757 were on paths absent from the recorded tree: 60.30%. Churn counts additions and deletions, including repeated changes to the same line. It measures maintenance history, rather than surviving programme size or runtime.

An earlier review reported 172,218 / 60.75%. The newer census could not reproduce that total and recorded its method and discrepancy. The census excerpt preserves the corrected figures and the earlier discrepancy.

§A model trained by counting

An earlier experiment learned next-byte probabilities by counting short sequences, then reading those counts with Kneser–Ney smoothing. No gradient training was involved.

On the recorded 18 MB training slice, it achieved 1.817 bits per byte, against 1.952 for a 1.71-million-parameter, two-layer byte Transformer. Lower is better: it means less surprise at the actual next byte. The record reports roughly 190 seconds of training against 3,785 seconds, on the same data, with top-choice accuracy 61.5% vs 58.3%.

This was an early byte-prediction experiment on a small corpus, recorded in June 2026. It suggested that useful learning could come from a much simpler computation. The measurement record preserves the comparison; it doesn't identify the CPU.

§Three geometries, zero, one or two channels

There is a neat mathematical result behind the pictures in the first essay. Ask how many ways we can turn a two-slot value into a real number while preserving addition, real scaling, multiplication and the unit.

So the same choice that gives rotation, shear or squeeze also decides whether those independent numerical channels exist. This is classical algebra, formalised in the channel classification source; the result concerns these structure-preserving maps, rather than arbitrary ways to read a pair.

§An earlier translation experiment

The earlier lifting work recorded one stored programme of 801,586 bytes becoming a 1,555-byte standalone ELF after reduction. Its native result agreed with Lean for that example. The striking part was that a stored computation could become a tiny executable.

The June 2026 record covers that example and the remaining work: nested and mutual recursion, indexed families and unresolved functions. Bringing whole existing programmes through this route is ahead.

Work with me

For research collaboration, funding or relevant contracts, see how to get in touch. The project pages describe the current work.