neuwirth/levineuwirth.org
neuwirth
/
levineuwirth.org
1
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

auto: 2026-08-30T08:51:44Z [skip ci]

This commit is contained in:
Levi Neuwirth 2026-08-30 10:51:44 +02:00
parent b855527eb4
commit 5b74013a6f
No known key found for this signature in database
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
content/work.md
View File

@ -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.