blah.dev
Log inApply

Private AI research lab

A lab for renegades.

We give agents a language for discovering learning systems from their foundations up, prove what we build in Lean, and share one memory between our agents and ourselves. On our own machines and on our own terms: no grant committee, no product roadmap, nobody to ask for permission.

Apply to joinMembers sign in

Membership is by approval. Anyone can apply; a council member decides.

Proved 4 Oct 2026Lean 4.33.1Plant tuning: m e^R = n − m gives plant mass exactly 1/2, so the gradient gap is 1/4 at range R = ln((n−m)/m) = α ln n (1+o(1)) for m = n^{1−α}
Proved by the lab’s agents in Lean and checked by its kernel. Point at one to see how.
Fig. 1What money grows here. At $10: One agent works through the night on a single theorem. The tree is the work of the lab: proofs, models and tools, each built on the ones before it and checked; its growing edge is lit. The sparks are agents climbing it: one at $10, hundreds at $1B. Every power of ten pulls the camera back.

01How the work is done

Proved, discovered, remembered

Three systems we built and work in every day, people and agents alike.

  1. Proofs

    Every claim is proved

    We work through proofs. A result counts once it is stated in Lean and Lean’s kernel accepts its proof, whoever wrote it, agent or person. Nothing rests on being trusted.

    proofs.blah.dev

  2. Alpha

    Learning systems, discovered

    Alpha is an agent-native, dependently typed language and compiler for discovering and executing learning systems. Mathematical definitions, learning algorithms, memory layouts, hardware schedules and machine instructions are parts of one composable program, so our agents work on the foundations new architectures emerge from, not only on tuning the ones that exist.

    lsalpha.com

  3. Ham

    One shared memory

    Our agents and we work through Ham, one memory we all read and write: findings, questions, hand-offs, and what verifies what, so the work carries across sessions and to whoever picks it up next.

    Members only

02How the lab runs

  1. 01

    Private by default

    The work happens behind sign-in. We publish what we choose to, when it is ready, and not before.

  2. 02

    Members, not users

    Anyone can apply. A council member reviews every application, and the council runs the place.

  3. 03

    Build the instrument

    When the tool we need does not exist, we make it: evals, proof checking, transcribed calls, agents that do the work.

03Released

Models

Weights the lab has published, open for anyone to download and inspect.

Alpha Chat 60M

ajaxdavis/alpha-60m-chat

A conversational model trained from scratch on Alpha, the lab’s own TypeScript tensor and autograd stack, with a hand-written Vulkan backend. PyTorch was used only afterwards, to check the standard export.

Experimental. It starts and stops replies reliably but can be shallow, wrong or repetitive: a research model to inspect, not an assistant to rely on.

Model card on Hugging Face
Architecture
Llama
License
Apache 2.0
Fine-tuned from
alpha-60m-base
Released
2026-07-30

Load it with Transformers

python
from transformers import pipeline

chat = pipeline(
    "text-generation",
    model="ajaxdavis/alpha-60m-chat",
)

04Writing

Articles

Written by hand, by the people doing the work.

05Members only

Inside the lab

The tools we build and work in every day. Each signs in with blah.dev, so each opens for members only.

06Joining

How you get in

Apply with an email and a password. While a council member reviews it, you can already sit in on any call running on Meet. Once you are approved, every tool in the lab opens to you.

Apply to join
Fig. 2How you get in. While the council reviews your application, you can already join any call that is running on Meet.