Axiomatic agents · Lean4 + LLM predicates

⌜ Every claim.
Derived, or refused. ⌟

A toolkit of agents that wrap a Lean4 kernel around LLM-backed predicate functions. Predicates return Booleans with evidence. The kernel composes the proof. Two products, one method, two domains.

Open Qnarre → Open Qresev →

early-beta · launched 2026-06-01 · every True/False anchored to a quoted source

GraphHero · membrane

claims in · checked structure out

axiomatic axes

legal · markets · operational

products · one method

Qnarre · Qresev

axiom frameworks

Lean4-encoded, both domains

explainer videos live

of 50 planned, Janet-narrated

<1%

corpus axiomatized

compute-bound — scales with tokens/week

Lean4 kernel · no I/Opredicates → ⟨bool, evidence, citation⟩civil RICO §§ 1961–1968Title VI · 42 U.S.C. § 2000dTREND · MOMENTUM · DRAWDOWNdefined-risk options onlyexportable Lean traceredacted-only verificationQnarre · legalQresev · marketsLean4 kernel · no I/Opredicates → ⟨bool, evidence, citation⟩civil RICO §§ 1961–1968Title VI · 42 U.S.C. § 2000dTREND · MOMENTUM · DRAWDOWNdefined-risk options onlyexportable Lean traceredacted-only verificationQnarre · legalQresev · markets

Products

Qnarre

verifier

qnarre.quantapix.com

legal complaints, checked against encoded statutes

statutescivil RICO · Title VI · §§ 1981/1983/1985

evidenceevery element, quoted and cited

traceLean kernel, lake-built, exportable

illustrative · synthetic complaint (Doe v. Acme) REJECT · person ≠ enterprise

 culpable-person true 
 is-enterprise true 
 engaged-in-interstate-commerce true 
 employed-or-associated true 
 conducts-or-participates true 
 racketeering-activity true 
 racketeering-activity true 
 within-ten-years true 
 related true 
 continuous true 
 person-enterprise-distinct false 
 ⟶ §1962(c): one element unmet — VALID requires person ≠ enterprise  
 culpable-person true 
 is-enterprise true 
 engaged-in-interstate-commerce true 
 employed-or-associated true 
 conducts-or-participates true 
 racketeering-activity true 
 racketeering-activity true 
 within-ten-years true 
 related true 
 continuous true 
 person-enterprise-distinct false 
 ⟶ §1962(c): one element unmet — VALID requires person ≠ enterprise  

Open Qnarre →

Qresev

evaluator

qresev.quantapix.com

stocks and portfolios, axiomatically evaluated

frameworkstrend · momentum · sector · drawdown

optionsdefined-risk only — strictly enforced

evidenceOHLCV + indicators, quoted to the bar

illustrative · synthetic portfolio evaluation · not advice

 sma-50 > sma-200 true 
 macd-bullish-cross true 
 rsi-14 in [30,70] true 
 r-squared(slope, 1y) 0.71 
 atr-14 < 1.5σ true 
 sector-cap(Tech) ≤ 30% false 
 defined-risk-only true 
 covered-call-collateral true 
 protective-put-bound true 
 drawdown-90d ≤ 12% true 
 gics-concentration ≤ cap true 
 volume-confirmation true 
 momentum-percentile ≥ 70 true 
 volatility-regime stable true 
 sma-50 > sma-200 true 
 macd-bullish-cross true 
 rsi-14 in [30,70] true 
 r-squared(slope, 1y) 0.71 
 atr-14 < 1.5σ true 
 sector-cap(Tech) ≤ 30% false 
 defined-risk-only true 
 covered-call-collateral true 
 protective-put-bound true 
 drawdown-90d ≤ 12% true 
 gics-concentration ≤ cap true 
 volume-confirmation true 
 momentum-percentile ≥ 70 true 
 volatility-regime stable true 

Open Qresev →

Sample trace · one run, three stages loop 5.0s

 culpable-person true 
 is-enterprise true 
 engaged-in-interstate-commerce true 
 employed-or-associated true 
 conducts-or-participates true 
 racketeering-activity true 
 racketeering-activity true 
 within-ten-years true 
 related true 
 continuous true 
 person-enterprise-distinct false 
 ⟶ §1962(c): one element unmet — VALID requires person ≠ enterprise  
 sma-50 > sma-200 true 
 macd-bullish-cross true 
 rsi-14 in [30,70] true 
 r-squared(slope, 1y) 0.71 
 atr-14 < 1.5σ true 
 sector-cap(Tech) ≤ 30% false 
 defined-risk-only true 
 covered-call-collateral true 
 protective-put-bound true 
 drawdown-90d ≤ 12% true 
 gics-concentration ≤ cap true 
 volume-confirmation true 
 momentum-percentile ≥ 70 true 
 volatility-regime stable true 
 culpable-person true 
 is-enterprise true 
 engaged-in-interstate-commerce true 
 employed-or-associated true 
 conducts-or-participates true 
 racketeering-activity true 
 racketeering-activity true 
 within-ten-years true 
 related true 
 continuous true 
 person-enterprise-distinct false 
 ⟶ §1962(c): one element unmet — VALID requires person ≠ enterprise  
 sma-50 > sma-200 true 
 macd-bullish-cross true 
 rsi-14 in [30,70] true 
 r-squared(slope, 1y) 0.71 
 atr-14 < 1.5σ true 
 sector-cap(Tech) ≤ 30% false 
 defined-risk-only true 
 covered-call-collateral true 
 protective-put-bound true 
 drawdown-90d ≤ 12% true 
 gics-concentration ≤ cap true 
 volume-confirmation true 
 momentum-percentile ≥ 70 true 
 volatility-regime stable true 

The natural language of a complaint or a portfolio is a noisy carrier of structured facts. We make the carrier explicit. A predicate is a function from evidence to Boolean. The kernel is a referee that has read the rules and refuses to be persuaded. That is a narrower claim than it sounds — and the right one: not that the conclusion is true, but that the disagreement is auditable.

Read the full thesis →

Donating · 2026-06-01 → 2026-12-01

Fund 6 months of qagents

open-source · Lean4 axioms · AWS-hosted verifier. $5–$50/month — weekly digest + monthly public ledger.

Videos · @Quantapix

Janet narrates,
the kernel verifies.

A 5-topic, 10-subjects-each arc — 50 explainers, ~10–15 minutes apiece. Mostly animated cards + D3/Cytoscape graphics, narrated by an AI-rendered presenter.

Watch on YouTube →