ai
-
Essay
Proof search is improving faster than the case for trusting it. Proof Broker puts a boundary between the two: Lean and Rocq send a goal out to external provers, take back a certificate with a graded trust tier, verify it at the boundary, and still require a proof term the home kernel checks. Nothing behind the boundary is trusted, so the search behind it can be as aggressive, heterogeneous, or unreliable as finding proofs requires. This essay sets out the architecture, what it makes possible, the evidence so far — 19 of 19 arithmetic obligations closed in a real verification project — and the research program that evidence opens.
-
Essay
A compute operator who claims to have run a particular model can be lying, and the logs that would settle it are written by the party under suspicion. VerInf produces zero-knowledge proofs of LLM inference, bounding the information in an output stream that a committed model does not account for. This living document details what the system certifies, what it does not, and what I contributed to it during the MARS V fellowship.
-
Essay
Software engineering does so little epistemic work that it hardly earns the name “engineering.” The field has never learned to distinguish provenance — where an artifact came from — from warrant — why anyone is entitled to rely on it. Authorship, a passing test suite, and a completed review are routinely mistaken for the second when they are only ever the first; libraries are the rare exception, where warrant is actually constructed and amortized across users who never read the source. LLM-generated code inherits neither comforting story, and the discomfort that provokes is not a new problem but the oldest one in the profession, finally felt without the anaesthetic that provenance usually supplies.
-
Essay
As we approach AGI, the increase in the ability of Artificial Intelligence models to infer a robust specification from a sparse prompt will lead to a devastating trend of homogeneity. We argue that this is the primary concern regarding the interaction of AI and human intelligence, rather than blanket claims that “AI reduces human cognitive ability.”
-
Essay
AI labs are likely deliberately reluctant to scale because they are aware that any imminient shift to locally run models as the norm would render their compute redundant. We take Anthropic as a principal case study to validate this hypothesis.