G6 LLC builds geometric models of threshold and switching behaviour in biological and physical systems — and proves them correct with a machine. Where conventional modelling fits parameters to data, our results are verified in Lean 4 against a proof kernel, so a reviewer can confirm them independently rather than take our word.
Three capabilities, all built on the same discipline: a claim is not finished until a machine has checked it.
Many systems — a molecular switch flipping, a surface saturating, a material yielding — turn on a critical value that is normally found by trial. We derive those thresholds from geometry, with no fitted parameters, and state in advance what result would prove us wrong.
We convert results proved on paper into machine-checked theorems in Lean 4. This is the discipline used for avionics and cryptographic code, applied to scientific models. The output is a file anyone can compile.
Every numerical claim we publish ships with the script that produced it, in the same deposit, with stated tolerances. No figure exists in our work that a reader cannot regenerate.
Capability claims are cheap. These two are checkable by anyone, in an afternoon, on their own machine.
We independently recompiled a recently published, field-defining mathematical disproof from scratch against the Lean kernel — 3,003 of 3,003 verification jobs passing, zero unproved steps. We claim no part of that result. The point is that the check was run, and can be run again.
We then audited our own published corpus for claims of machine verification, found two that did not hold, and published the failures on the front page of our journal with the files named.
The second matters more than the first. Work whose value is its auditability is only worth buying from a group that audits itself.
Our published work applies one geometric framework across biological and physical domains. All of it is open-access, permanently archived, and citable.
We work with laboratories, platform companies and research groups who need a model that can be defended, not only one that fits.
We are currently seeking a nucleic-acid bench partner to test three stated predictions in RNA switching and DNA surface amplification. Protocols and falsification criteria are published. Correspondence in English or Portuguese.