Axiomatic agents · Lean4 + LLM predicates
⌜
⌟
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.
Qnarre
verifier
legal complaints, axiomatically verified
statutes civil RICO · Title VI · §§ 1981/1983/1985
evidence every element, quoted and cited
trace Lean kernel, lake-built, exportable
00:00 is-enterprise → true
07:13 pattern-of-activity → true
14:26 predicate-act-mail-fraud → true
21:39 operation-or-management → true
28:52 use-of-mails → true
35:05 two-or-more-acts → true
42:18 continuity-or-relatedness → true
49:31 distinct-from-enterprise → false
56:44 investment-of-proceeds → false
03:57 conspiracy-1962d → true
10:10 recipient-federal-funds → true
17:23 discriminatory-effect → true
24:36 state-action → true
31:49 class-based-animus → true
38:02 is-enterprise → true
45:15 pattern-of-activity → true
52:28 predicate-act-mail-fraud → true
59:41 operation-or-management → true
06:54 use-of-mails → true
13:07 two-or-more-acts → true
20:20 continuity-or-relatedness → true
27:33 distinct-from-enterprise → false
34:46 investment-of-proceeds → false
41:59 conspiracy-1962d → true
48:12 recipient-federal-funds → true
55:25 discriminatory-effect → true
02:38 state-action → true
09:51 class-based-animus → true
Open Qnarre →
Qresev
evaluator
stocks and portfolios, axiomatically evaluated
frameworks trend · momentum · sector · drawdown
options defined-risk only — strictly enforced
evidence OHLCV + indicators, quoted to the bar
00:00 sma-50 > sma-200 → true
07:13 macd-bullish-cross → true
14:26 rsi-14 in [30,70] → true
21:39 r-squared(slope, 1y) → 0.71
28:52 atr-14 < 1.5σ → true
35:05 sector-cap(Tech) ≤ 30% → false
42:18 defined-risk-only → true
49:31 covered-call-collateral → true
56:44 protective-put-bound → true
03:57 drawdown-90d ≤ 12% → true
10:10 gics-concentration ≤ cap → true
17:23 volume-confirmation → true
24:36 momentum-percentile ≥ 70 → true
31:49 volatility-regime stable → true
38:02 sma-50 > sma-200 → true
45:15 macd-bullish-cross → true
52:28 rsi-14 in [30,70] → true
59:41 r-squared(slope, 1y) → 0.71
06:54 atr-14 < 1.5σ → true
13:07 sector-cap(Tech) ≤ 30% → false
20:20 defined-risk-only → true
27:33 covered-call-collateral → true
34:46 protective-put-bound → true
41:59 drawdown-90d ≤ 12% → true
48:12 gics-concentration ≤ cap → true
55:25 volume-confirmation → true
02:38 momentum-percentile ≥ 70 → true
09:51 volatility-regime stable → true
Open Qresev →
Live trace · one run, three stages loop 5.0s
PARSEPREDICATEELABORATE
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.
Read the full thesis →Public artifacts