Blog
Notes on verified claims calculation, formal methods, and how we build the software behind large-scale claims programs.
Categories
Posts
-
Why We're Building Claims Software in Lean
Every large claims program — a class-action settlement, a mass insurance payout, a compensation scheme — eventually comes down to software that decides who gets paid and how much. That software is usually written once, under deadline pressure, and trusted because it was "tested," not because anyone can show it is correct.
Read more -
Event Invitation: Uber Drivers and Mathematicians
Alongside the Data4Scientists and Data4Workers initiatives of our partners at PersonalData.IO, we are planning an informal gathering for Uber drivers and mathematicians in Geneva, to meet, talk, and think together about the math behind pricing, fairness, and trustworthy systems.
More details of the event will be announced on the forum page, here.
Read more -
What Is Lean?
Lean is a programming language and a proof assistant. It lets us write mathematical definitions, programs, and theorems in one environment, then ask a small trusted kernel to check whether a proposed proof really follows from the definitions and assumptions.
That makes Lean different from a calculator, a spreadsheet, or a conventional test suite. Tests check selected examples. A Lean proof can check a general statement for every input covered by its types and hypotheses. Automation may help discover the proof, but the kernel checks the result.
Read more -
Why Is Lean Revolutionizing Mathematics?
Calling Lean revolutionary is not a claim that mathematicians have stopped thinking or that every proof should be written by a machine. The deeper change is that formal proof makes a mathematical argument into a durable, checkable object that software can inspect and other people can replay.
Mathematicians have always checked proofs socially: by reading definitions, following arguments, trying examples, and asking colleagues to find gaps. Lean adds another layer of checking. The formal statement fixes what is being claimed, and the kernel checks that the proof follows from the imported facts and definitions.
Read more -
What Is the Navier–Stokes Controversy?
The Navier–Stokes equations describe how fluids move. They are central to physics and engineering, but one of the most famous open problems asks whether smooth solutions in three spatial dimensions always exist for smooth initial data, or whether a solution can develop a singularity in finite time.
This is one of the Clay Mathematics Institute's Millennium Prize Problems. The controversy is not simply whether a simulation looks plausible. It concerns a precise mathematical claim about existence, smoothness, and behavior for all relevant times and initial conditions.
Read more