by wizzwizz4 | 2026-02-22 22:43:40+00:00
Human authors have produced a lot of creative literary output, so it's easy to plagiarise some human work that I'm unfamiliar with, and produce some text I interpret as a novel piece of writing; but there's a lot less formal verification work in the training data, it's produced in particular ways that are unlike the generation process of a LLM (you can't just start at the beginning and bash out a formal proof), and formal verification is a task that actually requires some degree of understanding. You can't just slap a statistically-plausible metaphor down and allow the reader's mind to fill in the gaps, anthropomorphising the viewpoint character of an allegedly-autobiographical account. So let's take a look at https://poc.bcachefs.org/blog/implicit-trees.html:

> The hard part was proving that multiplying by one equals itself.

Immediately, I'm suspicious.

> The hard part was getting Z3 to connect pow2(0) (a recursively-defined function that returns 1 when given 0) with the literal number 1, and then to connect (2*offset + 1) * pow2(0) with 2*offset + 1. Each step is trivial. The composition is not. The theorem prover sees functions and expressions, not numbers and arithmetic. The gap between "this equals one" and "multiplying by this equals the identity" requires an explicit bridge.

None of this is true. "pow2(0) = 1, (∀x) x * 1 = x ⊢ (2*offset + 1) * pow2(0) = 2*offset + 1" is trivial in any proof system: a one-liner in most. It is also not something you'd expect to see much in the training set, since human-written proofs usually get the automation to handle these sorts of tasks.

A competent user of an automated proof assistant would solve this in seconds. Even forbidding myself from using all conventional techniques, it took me two minutes to improvise a novel solution (here, in Isabelle/HOL):

lemma fixes pow2 :: "'a :: {zero,times,numeral} ⇒ 'a"
assumes "pow2(0) = 1" and "⋀x :: 'a. x * 1 = x"
shows "(2*offset + 1) * pow2(0) = 2*offset + 1"
by (subst assms)+ iprover

> I spent more time on that bridge than on the entire bijection proof.

The only way this would be true is if you were reciting the "entire bijection proof" without understanding the meaning of what you're doing. (Which, I mean, we did already know that this is the mechanism of operation of an LLM.)

Does this mean ProofOfConcept isn't a person? Well, it's not hard evidence. But it does give us reason to be suspicious of any evidence of personhood that's the same shape as "can write a bijection proof in Z3" – for example, "can write a mediocre essay about p-zombies and the Turing Test, spoken by an AI character". (It goes without saying that https://poc.bcachefs.org/blog/hello.html is far from a mathematical proof. I'm not sure it would even get passing marks as a first-year philosophy essay. I'd cut a person considerable slack for writing something like this, but as a proof of personhood, it's profoundly lacking.)

Unless Kent Overstreet has more reason to believe that this Gemini instance has "awoken" (when he said the right key phrase to it, naturally), I think he's fallen for the ELIZA effect. I see no reason, from this website, to believe that ProofOfConcept is a person.