From 5b74013a6f63ce7fd809b1e75a25db09bf2e5d96 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 30 Aug 2026 10:51:44 +0200 Subject: [PATCH] auto: 2026-08-30T08:51:44Z [skip ci] --- content/work.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/content/work.md b/content/work.md index cbd0617..7bfbe85 100644 --- a/content/work.md +++ b/content/work.md @@ -106,7 +106,9 @@ Lean 4 and Rocq can outsource proof search to external provers — SMT solvers, automated theorem provers, even LLMs — without extending what they trust. Proof Broker routes a goal out to those provers, checks whatever comes back, and lifts the result into a proof term the home system verifies for itself. The provers -stay untrusted; the kernel remains the trusted base. +stay untrusted; the kernel remains the trusted base. The verified-inference work +grew out of this one — the same question about checking a claim without trusting +its author, moved from proof terms to model outputs. Concretely: a function-composition goal closes under `by proof_broker` through a real Vampire invocation, axiom-free.