About

Built from a problem that
refused to compromise.

Quantapix is an engineering practice. Two products, one method, two domains. The method: wrap a Lean4 kernel around LLM-backed predicate functions. Predicates return Booleans with evidence. The kernel composes the proof. The two products are Qnarre — an axiomatic verifier for legal complaints — and Qresev — an axiomatic evaluator for stocks and portfolios. Same kernel, different statutes, different OHLCV. Both launched as early-beta on 2026-06-01, each with a live trace: every True or False the system returns is anchored to a quoted source.

Real, life-altering problems are excellent system specs. They refuse to let you cheat. Years inside one such system — federal civil-rights litigation, pro se, against institutional defendants — turned out to be the same problem twice: how do you make a claim about a complex domain (statutes, markets) that an adversarial reader cannot reduce to your opinion?

The answer was the same in both places. Don't reduce it to opinion. Reduce it to a proof. Have a kernel that does no I/O check the proof. Have predicates — small, replaceable, audited — read the natural language the kernel won't touch. The result is a derivation, not a narrative; it survives a hostile reader because there is nothing to disagree with that isn't auditable.

This site is the engineering output. Code, schemas, traces, framework specs. The artifacts are versioned; the predicates are auditable; the kernel is open. If the method generalizes — and the same method already covers two non-overlapping domains — then the practice is the product and the products are demonstrations.

— Imre Kifor

femfas.net ↗ github.com/quantapix ↗ quantapix@gmail.com

Three of these links are one author — so don't take the author's word: the federal and appellate dockets are public (PACER). Check them.