Methodology
Posts
-
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 -
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