Technology

StartClaims brings ideas and methods from Lean — the interactive theorem prover and programming language used for formal mathematics and software verification — into the claims process. We also process Lean mathematical proofs directly when scientific credit claims or other controversies depend on whether a result follows from explicit assumptions.

We do not reduce law, insurance, or factual disputes to mathematics. We make the parts of a claim that can be formalized explicit — definitions, conditions, computations, and dependencies — so that professional judgment is easier to inspect, challenge, and reuse.

From plausible reasoning to checkable reasoning

Lean was built so that complex mathematical proofs and software properties can be checked by machine, using a small trusted kernel: sophisticated automation may propose a chain of reasoning, but a compact, auditable checker decides whether it actually follows from the stated assumptions.

StartClaims applies that same architecture to claims and scientific controversies. Instead of a calculation living only in a spreadsheet or a script — trusted because it "looked right" or passed a handful of test cases — every rule and formula is written down as an explicit specification, and the software that runs it is proven to match that specification, for every input.

For a concrete illustration of what a formal specification and proof actually look like, here is a small, self-contained example: a timeliness rule that might govern whether a claim was filed within a program's claims window.

structure Claim where claimant : String amount : Nat filedAt : Nat -- days since the claims period opened deriving Repr /-- A claim is timely if it was filed within the claims window. -/ def isTimely (windowDays : Nat) (c : Claim) : Bool := c.filedAt ≤ windowDays

This kind of definition is trivial by itself. What matters is that every rule in a real claims program — eligibility windows, caps, offsets, proration, multi-tier formulas — can be built out of small, explicit, checkable pieces like this one, composed together and proven correct as a whole, rather than reimplemented by hand for every new claimant or every new program.

Proofs as evidence in scientific controversies

A Lean proof can be treated as a structured evidence object: its theorem, definitions, imported results, tactics, and assumptions can be inspected and replayed. Processing that proof helps distinguish a proved mathematical statement from an informal interpretation, and shows where two accounts share a result or diverge. This can inform disputes about priority, authorship, contribution, or the scope of a scientific claim, without pretending that a kernel can decide every question about scientific credit.

A vocabulary for claims

Formalizing a claim requires a shared vocabulary between the people who understand the rules and the people who encode them. We use a small set of concepts consistently across engagements:

  • Evidence item. A source supporting one or more facts — a contract, an account record, an invoice, a policy document, correspondence.

  • Fact. A normalized proposition extracted from or established by evidence — a date, an amount, an event, a status.

  • Rule. A condition, definition, formula, or legal/policy proposition used in reasoning.

  • Proof obligation. Something that must be established for a conclusion to follow.

  • Evidence gap. A proof obligation for which support is currently insufficient.

  • Derivation. A checkable chain connecting premises to a conclusion.

  • Claim template. Reusable logic shared by a class of claims.

  • Claim instance. An individual claimant's facts and evidence applied to a template.

  • Dependency graph. The graph showing what each conclusion depends on.

  • Version. The exact state of facts, rules, and calculations at a given point in time.

These concepts are what let StartClaims scale reasoning across many claims without flattening individual claimants into a single average case.

The role of AI

AI is useful for building claims, but it is not the source of trust. In our architecture, AI can propose; sources support; formal checks constrain; and humans decide.

Concretely, AI can help extract candidate facts from documents, classify evidence, suggest which claim template may apply, match evidence to proof obligations, draft plain-language explanations, flag anomalies across large groups of cases, and even help draft rules or formal propositions — always subject to review and to the same checking process as everything else. An AI-generated answer is never treated as self-authenticating.

Trust and provenance

For any claim, we aim to preserve, end to end:

  • the original source, who supplied it, and when;

  • the transformations applied to it;

  • the extracted facts, and whether they are disputed or agreed;

  • the rule and calculation versions in effect;

  • the human review steps and machine checks performed;

  • the full dependency path from a conclusion back to its evidence.

Not just an answer — a path back to the evidence.

Frequently asked questions

Does this replace legal or actuarial judgment? No. Formal verification confirms that software matches a specification; deciding what that specification should say remains a legal and actuarial question. We work closely with counsel, actuaries, and claimant representatives throughout rule intake.

What if the rules change mid-program? Because the rules are a formal specification rather than scattered logic, a change is made once, re-verified, and the effect on every downstream claim is immediately visible.

What does "generating claims" mean in practice? Once a template is formalized and verified, we use it to produce actual claim determinations and outcomes for real claimants, rather than handing over software for someone else to reimplement from scratch.