In all my sixty-seven years
I don't think I have ever been
So flummoxed, to the point of tears,
As by proof verifier Lean.
I have a lot of proofs that I
Have written down in F.O.L.
I thought, if I could verify
That they're correct, that would be swell.
I first succeeded in installing
Platform Visual Studio,
The interface, although appalling,
Sort of works. I'm good to go.
The next step, clearly, was to study
Theorem Proving in Lean 4
And so, this aging fuddy-duddy
Read that esoteric lore.
Though not without complaints and gripes
I fairly easily got through
The theory of dependent types
The book presents in chapter two.
But when I got to chapter three
The home of "Proof", "Implies", and "Prop",
It utterly bewildered me.
So, sadly, I was forced to stop.
The theory claims, "If p then q"
Is actually a function space,
But that outlandish point of view
Is one that I cannot embrace.
Abandoning this futile quest,
I turn to other targets now.
I'm leaving Lean — I'm sure that's best —
To geniuses like Terry Tao.
This is part of the collection Verses for the Information Age by Ernest Davis