Methodology
The real product is a research pipeline. Hearing loss is where we point it first.
MISHA is a bet that a disciplined, AI-augmented research pipeline can compress the early, expensive part of science. We test it in the open, on problems where the answer is checkable, and point it at STRC hearing loss. The method is the point. The disease is the proof.
How it started
The first real test was STRC. I ran the computational analysis on my son's gene and sent it, unannounced, to a leading hearing-genetics lab at Harvard and to researchers in Shanghai. The responses came back serious and engaged.
That flipped the idea. A pipeline that earns the attention of credible scientists on two continents can do the same across rare disease, for families who will never cold-email Harvard themselves.
Computation is a lever, not an oracle
The model is confident even when it is wrong. So the pipeline is built around verification: ground truth first, computation second, every claim checked against real measured sources before it moves. When anyone can generate a plausible hypothesis, the scarce thing is one that has already been checked. We hand a researcher the survivors, not the noise.
Why we prove it on mathematics first
Math is the honest proving ground, because you cannot argue with a proof. We point the pipeline at long-open problems, the kind Erdős posed, and formalize every step in Lean 4 so a proof kernel checks it line by line. Eleven of those formalizations are merged into lean-pool, the community pool of machine-checked results around the Erdős problems, covering Moser's distinct-subset-sums inequality, Conway-Guy gap rigidity, the convex-octagon case of Erdős Problem 97, and the known Hadwiger-Nelson bounds, among others. A list-coloring compactness result is under review at Mathlib, the main mathematics library for Lean.
The honest status: no famous problem is solved. What exists is machine-verified partial progress, finite cases and audited certificates, one preprint, and a public log of what did not work. A pipeline you can only see when it wins is a pipeline you cannot trust.
The tools we depend on get the fixes back
The pipeline runs on open-source tools I did not build: RDKit for chemistry, Paraphase for calling the STRC gene itself against its pseudogene, fgbio for sequencing quality control, OpenMM for molecular dynamics, MDGP.jl for the distance geometry behind structure prediction. When the pipeline hits a bug in one of them, the fix goes upstream, not into a private patch. Fixed once, it stays fixed for every lab using the same tool.
This is the cheaper path, not charity. A workaround in a private fork has to be re-applied on every upgrade, forever. A fix merged upstream costs the effort once and speeds up this pipeline and every other lab's. Better field tools and a faster STRC pipeline are the same fix.
The honest status, kept current: merged in RDKit (coordinate validation before distance-geometry embedding) and SageMath (faster p-adic L-series precision bounds). Under review: two Paraphase changes that make STRC copy-number calls more honest about ambiguity, plus fixes in fgbio, OpenMM, SymPy, and MDGP.jl.
The same pipeline, pointed at hearing genetics
On STRC and adjacent hearing-loss genes, the pipeline does what it does on a math problem: rank the hypotheses worth testing, predict the structures with AlphaFold3-class models, and find the druggable pockets, before anyone spends wet-lab money. It also hardens the tools clinical labs use to genotype STRC itself. The outputs are public. This is the engine inside the Research Lab program.
Why this matters for a foundation
A one-person foundation cannot ask you to trust its polish. It can show a method that works on checkable problems, run it in the open, and let the record speak. Build the pipeline once, prove it honestly, point it at the diseases the market leaves behind.