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.

What does this have to do with claims?

A claim is not only its conclusion. It also has evidence, definitions, rules, calculations, assumptions, and a path of reasoning connecting them. For example, a compensation claim might depend on a person's working hours, the meaning of eligible work, a rate, a cap, and an exception in the programme rules.

Lean can help represent the formalizable parts of that chain. It can state a rule precisely, define a calculation, and check that an implementation matches the specification. It cannot decide whether a witness is credible, whether a contract should be interpreted one way or another, or what a court should do. Those remain matters for people and institutions.

The role of Lean at StartClaims

We use Lean to make some important claims checkable: which facts are being used, which rules are applied, which calculations follow, and which assumptions are still open. The result is not a machine-made answer detached from context. It is a more inspectable chain from evidence to conclusion.

That distinction matters whenever a claim is repeated at scale. A programme may apply one formula to thousands of people, but each person still has their own evidence and circumstances. Lean helps verify the shared logic while the individual record remains visible.