Edition 021 flagged the verification gap: AI is producing results faster than anyone can check them. This week, three responses showed up. Tao's Palomar registry gives Lean proofs a submission and review infrastructure. BioNexus grades whether an agent's biology analysis is scientifically valid. Lea keeps the mathematician in the loop during formalization. On the production side, Anthropic's protein-design agent and Inherent's Faraday keep pushing the pace.
Palomar: a registry of Lean-verified mathematics
Terry Tao, August 18 2026
A preprint-server equivalent for Lean proofs, created because AI-generated proofs are proliferating and checking that a repo actually proves what it claims (no extra axioms, no cheats, typecheck passes) is non-trivial.
Lea: an open-source Lean 4 theorem-proving agent
Chinmay Hegde et al. (NYU), August 14 2026
A DARPA-funded theorem-proving agent with a full UI, backend visibility, and an Overleaf extension that auto-formalizes LaTeX to Lean while you write, designed to keep the mathematician in the driver's seat rather than automate the proof end to end.
BioNexus: a scientific reliability layer for agentic biology
Herry Z., August 2026
An open-source layer between AI coding agents and bioinformatics workflows that grades conclusions (PRELIMINARY through REPLICATED, or ABSTAIN) and refuses to proceed when preconditions are not met, encoding the difference between knowing how to run an analysis and knowing when it is valid.
How Claude is accelerating protein design and analytical chemistry
Anthropic, August 18 2026
Claude ran a full protein-binder design pipeline autonomously (1,320 designs, 354 confirmed binders, hit rates roughly double the typical baseline), with wet-lab validation by Adaptyv Bio and Twist Bioscience, though this is a first-party announcement and not peer reviewed.
Training AI scientists to replicate research
Damon Falck et al. (Inherent), arXiv, August 13 2026
A 27B-parameter agent trained via reinforcement learning on 310 paper-replication tasks outperformed larger frontier models, suggesting that research reproduction (read the methods, write the code, reproduce the figures) may be automatable before original research is.
When errors become consensus: science's self-correction can no longer keep up
The Scholarly Kitchen (Jason Hu), August 17 2026
Retracted papers, paper mills, and AI recursion are creating what Hu calls "synthetic consensus," where claims gain credibility through repetition rather than verification, and the rate of error creation now outpaces the field's capacity to correct.
AI can find the article. Can it tell which version it used?
The Scholarly Kitchen (Patrick Hargitt and Steve Smith), August 19 2026
AI systems pulling articles from preprints, publishers, and repositories often cannot tell which version they used, turning version ambiguity from a discovery problem into a provenance problem that existing persistent identifiers alone do not solve.
Qualitative research in an era of artificial intelligence
Annual Review of Sociology (Corey M. Abramson et al.), 2026
A peer-reviewed review of how AI and LLMs are reshaping qualitative methods like ethnography and interviewing, one of the first discipline-level assessments from outside the AI-in-STEM cluster.