Independent researcher. Fundamental mathematics first, applied through open-source tools for rare genetic disease.
I formalize proofs in Lean and use that as a test bench for an AI research workflow: Lean checks a proof term against its stated assumptions, so a claim either type-checks or it does not.
The repos below apply the same workflow to rare genetic disease: computational tools and source-linked analysis, published so specialists can inspect the methods. Biological experiments, clinical data, and specialist review still decide what holds up. None of that happens in this code.
The generator discovers every public pull request in Vilin97/lean-pool authored by lyfar, then reads its current GitHub evidence. Reviewed entries use explicit claim-scope classifications. A new pull request appears automatically as SCOPE PENDING until its claim boundary is classified. Each row keeps Lean builds, automated Lean Pool editorial review, formal human review, claim scope, and PR state separate.
EGRS75 merged PR #179 | Lean Pool PRs by lyfar | Generator and scope classifications | Test fixture
| Work | Evidence | Boundary |
|---|---|---|
| STRC Research | Public computational work on STRC-related DFNB16 hearing loss | Preclinical hypotheses with no therapeutic claim |
| Distance Geometry in Lean | Source-linked Lean formalization and draft PR #271 | A test of the research workflow in mathematics |
| EGRS75 in Lean | Lean build record, automated review, and maintainer merge | A formalization of a known theorem |
| Genomic Variant Research | Auditable variant-analysis workflow | Research support; clinicians make diagnoses |
I welcome mathematical review, AI workflow audits, rare-disease expertise, and partners who can support experimental validation.