verification
Process reward models: grading the working, not just the answer Lesson
A process reward model scores each step of a model's reasoning rather than only the final answer, which makes it possible to catch a wrong turn even when the conclusion happens to come out right - and to tell a lucky guess apart from genuine reasoning.
DeepSeek is serving a model called V4.1 Flash that it has not announced News
A model identified as deepseek-v4.1-flash began answering on DeepSeek's API under an ID carrying its own expiry date, but the company has published no model card, no technical report and no changelog entry, and its predecessor V4 Pro remains the latest documented release.
Discovery Loop gets ten AI-assisted circle-packing candidates accepted by Packomania News
Discovery Loop used Claude Fable 5.1 to revise a solver and produced ten circle-packing candidates accepted by Packomania in an eight-hour, $27.72 consumer-PC run.
Property-based testing: test the rule, not just the examples Lesson
Property-based testing generates many inputs automatically and checks general rules that software should always obey, such as round trips, invariants, and equivalence under harmless transformations; it finds edge cases that example-by-example unit tests often miss.
Program synthesis: making a computer write the program from the specification Lesson
Program synthesis is the task of automatically constructing a program that satisfies a specification such as examples, types, tests, or logical constraints; it matters because a verifiable specification can turn programming from writing every instruction into searching for a correct implementation.
Claude helped set two elliptic-curve rank records in four days News
A public leaderboard run by an NSF mathematics institute recorded new rank records for elliptic curves on August 20 and August 23, both credited to Claude working with mathematicians Levent Alpoge and Ava Howell.
An agent that cannot mark its code done until the hardware agrees News
A new system for generating industrial controller code refuses to let the model declare success until the specification, the compiler and a live runtime all independently agree, exposing a wide gap between code that compiles and code that behaves.
A record elliptic curve now lists Claude as a collaborator News
The canonical public record page for elliptic curve ranks has added a 2026 entry at rank 30 or higher, publishing an explicit curve with 30 independent points, and the attribution credits Claude alongside two named researchers, though no primary source describes what the model actually did.
An AI agent rewrote 189 files in a 717,000-line codebase and nobody read the code News
A developer documented an AI coding agent dismantling a core architectural assumption across a 717,725-line production application over three days for $2,430, with 201 defects corrected across 31 automated audit passes and no human review of the generated code.
The viral Riemann result an AI supposedly proved is not in the literature News
A widely shared claim that Claude raised the proven fraction of Riemann zeta zeros on the critical line from 41.6 to 67.2 percent does not match any published result; the closest paper says the two-thirds figure follows only if an assumption nobody has removed can be removed.
Figure's viral ladder climb is a two-hour stair timelapse News
A widely shared clip of Figure's F.03 humanoid was reposted as an autonomous ladder climb; the company's own post describes a timelapse of repeated stair traversal that is helping move its robots closer to full autonomy.
A frozen 12B model answers already-solved problems at zero generation tokens News
A technical report describes a 12-billion-parameter model whose weights never change but which answers new instances of nine previously solved problem families with no generated tokens at all, scoring 180 out of 180 by executing verified stored procedures instead of reasoning again.
AI Helped Crack a Famous Math Conjecture, and Humans Verified It in Lean News
Mathematicians found an explicit counterexample disproving the Jacobian conjecture in three dimensions, checked partly with an AI chatbot and formalized in a Lean proof, while two other viral AI-math claims remain unverified.
A Mathematician Posts a Counterexample to a Famous Conjecture, Crediting an AI Model News
Mathematician Levent Alpoge posted a hand-checkable counterexample to the Jacobian conjecture and credited the AI model Fable; the math is independently auditable, but the AI's actual role is not documented.
AI is now solving hard math and physics problems faster than humans can formally check them News
A widening 'verification lag' is emerging as AI produces candidate solutions to hard problems faster than experts can formally verify them - physicist Yuji Tachikawa reports Fable cracked a six-month research blocker, while a GPT-5.6 Erdos claim circulates without peer review.
'Dockerless' verifies AI code patches by reading the repo instead of running it News
A new method called Dockerless judges whether an AI's code patch is correct by having an agent explore the repository for evidence rather than executing tests in a Docker container, enabling a fully environment-free training pipeline for coding agents.
TorchLean Tool
A Lean 4 framework for formalizing, executing and verifying neural networks, with typed tensors, exact and finite-precision semantics, verified reverse-mode differentiation, and CROWN/LiRPA-style bound checking. Early and CPU-bound by its authors' own account, but it is the most concrete attempt yet at machine-checked robustness guarantees.
Lean comparator Tool
The Lean toolchain component used to independently check the formalization behind Anthropic's zeta-function result. Useful to anyone who wants machine-verified mathematics rather than a persuasive argument.
Galahad verified-reuse testbench Tool
Public testbench for the frozen-12B verified procedure cache, where a solved and independently verified problem family is answered on later instances at zero generation tokens, bit-exact. Worth poking at to understand what the claim does and does not cover -- the engine source, configuration and raw artifacts are withheld, so this demo plus the bench repo is the only inspectable surface.
Elliptic Curve Rank Leaderboard Tool
An NSF-funded public record of high-rank elliptic curves, where every submission publishes its witness points, commentary and edit history, and offers a JSON endpoint so anyone can verify a claimed record independently.
Claude Content Credentials Checker Tool
Free browser tool that reads C2PA content credentials embedded in image, video, and audio files, up to 100 MB across 17 formats. It runs locally and the file never leaves your machine. Important limitation stated on the page itself: it reads the credential only, and cannot tell you whether an AI was involved in creating content that carries no credential.