When Machines Design, Prove, and Discover
The frontier this week is autonomy with accountability. AI models are now running full protein-design campaigns and generating functional molecules from plain language, while a parallel movement in formal methods insists that machine-generated work be mechanically proven, not merely sampled. We pair the boldest experiments in autonomous discovery with the verification infrastructure racing to keep pace.
Autonomous Discovery at the Bench
Both items describe systems that compress the protein design cycle by letting computational models—rather than human experts—make the core design decisions, from selecting targets to generating candidate sequences. In each case, functional validation in the wet lab confirmed that machine-driven design can match or exceed outcomes typically associated with expert-led, iterative approaches, whether measured through binding affinity or catalytic activity. They differ, however, in what triggers the design process and what kind of molecule results: one uses an AI model to autonomously plan and execute binder discovery campaigns against specific antigenic targets, relying on external high-throughput platforms to handle the experimental bottleneck, while the other uses a language-driven generative model to produce entirely new proteins directly from textual functional descriptions, spanning fluorescence, catalysis, and metabolic roles. The former demonstrates end-to-end autonomy across an experimental pipeline reliant on specialized instrumentation, whereas the latter demonstrates a novel input modality—natural language—as a general interface for specifying protein function.
Carterra enables Anthropic’s autonomous AI protein design study
Anthropic's Claude models autonomously ran de novo protein binder design campaigns against 15 challenging targets—selecting epitopes, running open-source design tools, and ranking candidates without human input into design decisions—with wet-lab validation handled by Twist Bioscience and Adaptyv Bio using Carterra's high-throughput SPR platforms. The study, published August 18, 2026, reports hit rates exceeding prior methods, with binder generation taking days rather than the weeks-to-months typical of human-led design, effectively shifting the bottleneck from design to experimental validation. Carterra's array-based approach reportedly compresses large-scale affinity/kinetics measurement into a small number of unattended runs using roughly 1% of the antigen sample required by legacy SPR systems, enabling head-to-head comparisons on shared arrays: in one case, Claude's best RBX1 binder measured 3.9nM affinity versus 45nM for a prior open-competition winner under identical conditions. Running human, mouse, and cynomolgus target variants in parallel also let Anthropic capture species cross-reactivity data as part of the primary dataset rather than requiring a separate follow-up study.
Toward De Novo Protein Design from Natural Language
Pinal is a 16-billion-parameter generative model that designs proteins directly from natural-language functional descriptions, trained on a synthetic corpus of 1.7 billion protein-text pairs, bypassing the usual reliance on homologous templates or family-specific design expertise. In wet-lab validation across four distinct functional classes—a fluorescent protein, a PET hydrolase, an alcohol dehydrogenase, and a metabolic H-protein—all four de novo designs were functionally active, with both enzymes showing measurable catalytic turnover. Notably, the designed H-protein outperformed its natural counterpart by 1.7-fold. The results demonstrate that free-text functional descriptions can act as a programmable interface for protein design, pointing toward a shift from iterative modification of existing proteins to direct generation of novel functional molecules from conceptual specifications.
Proof as the New Quality Gate
Both items describe efforts to replace human judgment with mechanical verification as the arbiter of correctness in an era when AI systems generate code and proofs faster than people can review them. In each case, the underlying concern is the same: sampling-based checks—unit tests, code review, peer review—no longer scale to the volume and opacity of machine-generated output, so Lean is being pressed into service as an infrastructure layer that can certify correctness exhaustively rather than spot-check it. The two differ in domain and in what the human is still asked to do: Pant's account centers on software engineering, where humans retain responsibility for writing specifications while AI produces implementations that Lean-based tooling checks against them, as illustrated by AWS's own production systems. Tao's Palomar, by contrast, targets mathematical proof itself, building a submission and registry system where the human contribution shrinks to framing an informal statement and challenge file, with typechecking and an LLM check handling verification—while explicitly disclaiming that this substitutes for peer review of novelty or truth.
AWS's Varun Pant: AI Agents Write Code, Lean4 Must Prove It
AWS engineer Varun Pant, speaking on the AI Engineer podcast, argues that agent-generated code has broken traditional quality gates (human review, unit tests, LLM-as-judge) because these methods only sample inputs, while formal verification with Lean4 proves correctness across all inputs. He describes an emerging division of labor he calls "back-driven development": humans write specifications, AI writes implementations, and formal tools mechanically prove the two match, shifting the critical bottleneck from code review to specification review. Concrete evidence includes AWS's Cedar authorization language, which runs about 100 million differential random tests nightly between its Lean spec and Rust implementation before shipping; the Andreo project, where an AI converted zlib into 32,000 lines of Lean proof independently verified by a kernel; and Strata, an AWS tool aiming to generalize this Lean-based verification workflow across programming languages.
Palomar – a registry of Lean verified mathematics
Terence Tao announces the launch of Palomar, a new registry for Lean-verified mathematics proofs, incubated by the Lean FRO and ICARM, designed as a "preprint server" analogue for formal proofs amid a surge of AI-generated Lean formalizations. Submissions must include a human-readable "challenge file" stating the result, a "solution module" proving it, and a "formalization.yaml" describing the result informally; the registry then runs two checks—a mechanical typechecking/matching verification via the Lean tool Comparator, and a non-deterministic LLM-based check that the informal description matches the formal statement. Tao stresses these checks are not equivalent to peer review for novelty or correctness, and demonstrated the submission process himself using his recent Lean formalization of the proof of Sendov's conjecture. The registry is now open to both human- and AI-generated submissions, old and new, with discussion hosted on a dedicated Zulip channel.
Simulating Biology at Scale
I ran Boltz-2 100 million times to check if it can simulate cell biology
A Recursion researcher describes a year-long side project running Boltz-2 and AlphaFold-Multimer co-folding at massive scale on pre-emptible GPUs, generating "affinity-prints"—a dataset of 100 million predicted protein-ligand and protein-protein interactions spanning 9,000 targets and 500k ligands—to test whether cell-scale biology can be approximated from bottom-up interaction simulation rather than top-down generative modeling. The key move is pairing these raw co-folding outputs with Recursion's proprietary phenomics maps (built from gene-knockout microscopy assays) to filter which of the billions of possible interactions are actually biologically meaningful, since exhaustive co-folding across the human proteome is computationally intractable without this triage step. Concrete outputs include a minimal "Virtual Cell" model with just 6 trainable parameters that reconstructs phenomics similarity maps from thresholded, PPI-pooled affinity signatures; a data-driven ligand-scoring metric (Lig2Cell) that reportedly beats Lipinski/QED rules for hit enrichment; and an analysis finding that a protein's druggability depends more on subcellular localization, function, and lipid coverage than on its structural class. The author frames all of this as early-stage proof-of-concept, not validated science, but argues that combining scaled inference compute with biological ground-truth maps—especially as affinity prediction gets cheaper (citing a claimed 20x speedup with a model called Nesso-1)—could open a path toward co-fol