Alex Nelson
@pqnelson.bsky.social
Mathematician, software engineer. Obsessed with everything about proof assistants.
AMS Subject Class.: 68V15, 68V20, 20Exx.
AMS Subject Class.: 68V15, 68V20, 20Exx.
Exercise: implement a proof checker for the Hilbert proof calculus from Bourbaki's foundations (a Hilbert epsilon calculus) using plain TeX as the implementation language.
November 30, 2025 at 4:25 PM
Exercise: implement a proof checker for the Hilbert proof calculus from Bourbaki's foundations (a Hilbert epsilon calculus) using plain TeX as the implementation language.
It's amazing to me how much faster plain TeX is than LaTeX.
I have a medium-sized project, producing 72 pages of output, run in a 1.074 seconds in plain TeX.
LaTeX takes about 15 times longer on a comparably sized project.
And plain TeX is *stable*.
I have a medium-sized project, producing 72 pages of output, run in a 1.074 seconds in plain TeX.
LaTeX takes about 15 times longer on a comparably sized project.
And plain TeX is *stable*.
November 28, 2025 at 7:18 PM
It's amazing to me how much faster plain TeX is than LaTeX.
I have a medium-sized project, producing 72 pages of output, run in a 1.074 seconds in plain TeX.
LaTeX takes about 15 times longer on a comparably sized project.
And plain TeX is *stable*.
I have a medium-sized project, producing 72 pages of output, run in a 1.074 seconds in plain TeX.
LaTeX takes about 15 times longer on a comparably sized project.
And plain TeX is *stable*.
Read later, this seems like a good "second or third book" on finite group theory after I Martin Isaacs's book and Aschbacher's book...
arxiv.org/abs/2511.18392
arxiv.org/abs/2511.18392
Invitation to finite groups
This is an introduction to the finite groups, with focus on the groups of permutations and reflections, and more generally, on the finite groups of unitary matrices. We first discuss the basics of gro...
arxiv.org
November 25, 2025 at 3:59 PM
Read later, this seems like a good "second or third book" on finite group theory after I Martin Isaacs's book and Aschbacher's book...
arxiv.org/abs/2511.18392
arxiv.org/abs/2511.18392
I helped Dr Nipkow catch a few typos in his chapter on Red-Black trees (and elsewhere). In fact, I think this is the first book I am thanked in the preface 😇
Just out: Functional Data Structures, edited by Tobias Nipkow
November 25, 2025 at 2:52 PM
I helped Dr Nipkow catch a few typos in his chapter on Red-Black trees (and elsewhere). In fact, I think this is the first book I am thanked in the preface 😇
Looking at Grothendieck's [Système de pseudo-droites]: notes manuscrites (1983-1984, s.d.). Cote no 154, 175 pages...and my goodness, that's terrible handwriting. Or is it just me? Does anyone find this legible?
grothendieck.umontpellier.fr/archives-gro...
grothendieck.umontpellier.fr/archives-gro...
Archives Grothendieck » Archives Grothendieck
grothendieck.umontpellier.fr
November 22, 2025 at 2:42 AM
Looking at Grothendieck's [Système de pseudo-droites]: notes manuscrites (1983-1984, s.d.). Cote no 154, 175 pages...and my goodness, that's terrible handwriting. Or is it just me? Does anyone find this legible?
grothendieck.umontpellier.fr/archives-gro...
grothendieck.umontpellier.fr/archives-gro...
My god, some zealous grad students in the Lean community don't understand satisfiability is a predicate in the metalanguage, and results concerning soundness and completeness are metatheorems. "They're theorems!"
...not in the object logic, they're not...
...not in the object logic, they're not...
November 22, 2025 at 1:06 AM
My god, some zealous grad students in the Lean community don't understand satisfiability is a predicate in the metalanguage, and results concerning soundness and completeness are metatheorems. "They're theorems!"
...not in the object logic, they're not...
...not in the object logic, they're not...
I wonder how many of my readers recognize the allusion with the section title "Precedence lost and Precedence regained"...
November 18, 2025 at 10:35 PM
I wonder how many of my readers recognize the allusion with the section title "Precedence lost and Precedence regained"...
I realized there are three audiences I'm writing for, but failing to actually communicate to each of them:
(1) Mathematicians interested in *using* proof assistants
(2) Mathematicians interested in *building* proof assistants
(3) People interested in Foundations of Mathematics
...and maybe more?
(1) Mathematicians interested in *using* proof assistants
(2) Mathematicians interested in *building* proof assistants
(3) People interested in Foundations of Mathematics
...and maybe more?
November 15, 2025 at 9:57 PM
I realized there are three audiences I'm writing for, but failing to actually communicate to each of them:
(1) Mathematicians interested in *using* proof assistants
(2) Mathematicians interested in *building* proof assistants
(3) People interested in Foundations of Mathematics
...and maybe more?
(1) Mathematicians interested in *using* proof assistants
(2) Mathematicians interested in *building* proof assistants
(3) People interested in Foundations of Mathematics
...and maybe more?
Reposted by Alex Nelson
Once you start thinking of AI as a war on humanity, on human thought, on human inquiry, on human labor, on nuance and critical thinking, it slots in pretty seamlessly with the right wing ideological project, oligarchical political projects, big tech's political projects, etc
November 6, 2025 at 4:48 PM
Once you start thinking of AI as a war on humanity, on human thought, on human inquiry, on human labor, on nuance and critical thinking, it slots in pretty seamlessly with the right wing ideological project, oligarchical political projects, big tech's political projects, etc
Don't forget:
"Vielbein" refers to the frame field in *arbitrary* number of dimensions.
"Vierbein" refers to the frame field specifically in *four* dimensions.
...because we couldn't use "frame field", that'd be crazy talk.
"Vielbein" refers to the frame field in *arbitrary* number of dimensions.
"Vierbein" refers to the frame field specifically in *four* dimensions.
...because we couldn't use "frame field", that'd be crazy talk.
November 6, 2025 at 2:05 AM
Don't forget:
"Vielbein" refers to the frame field in *arbitrary* number of dimensions.
"Vierbein" refers to the frame field specifically in *four* dimensions.
...because we couldn't use "frame field", that'd be crazy talk.
"Vielbein" refers to the frame field in *arbitrary* number of dimensions.
"Vierbein" refers to the frame field specifically in *four* dimensions.
...because we couldn't use "frame field", that'd be crazy talk.
Reposted by Alex Nelson
I just learned the inventor of Metamath, Norm McGill, passed away a few years ago, in 2021.
I'm rather heartbroken to learn it.
I'm rather heartbroken to learn it.
November 2, 2025 at 1:07 AM
I just learned the inventor of Metamath, Norm McGill, passed away a few years ago, in 2021.
I'm rather heartbroken to learn it.
I'm rather heartbroken to learn it.
"77.4.17 Remark: An optimistic note. The author's search for truth doesn’t amount to a hill of beans in this crazy world...
November 1, 2025 at 12:32 AM
"77.4.17 Remark: An optimistic note. The author's search for truth doesn’t amount to a hill of beans in this crazy world...
We can have a module over a (unital, associative) ring. Everyone knows this.
But we can also have a module over a monad, or a Lie algebra, or a non-unital ring.
What's the most general setting where we can define a module?
But we can also have a module over a monad, or a Lie algebra, or a non-unital ring.
What's the most general setting where we can define a module?
October 26, 2025 at 9:53 PM
We can have a module over a (unital, associative) ring. Everyone knows this.
But we can also have a module over a monad, or a Lie algebra, or a non-unital ring.
What's the most general setting where we can define a module?
But we can also have a module over a monad, or a Lie algebra, or a non-unital ring.
What's the most general setting where we can define a module?
Random question: there's a cayote on campus which appears at random times. I've run across it (it's the size of a medium-small dog, or a little smaller than a wolf). Security says to call them if we see it...but what am I *supposed* to do with Cayotes? Play dead? Climb a tree? Don't move?
October 22, 2025 at 12:19 AM
Random question: there's a cayote on campus which appears at random times. I've run across it (it's the size of a medium-small dog, or a little smaller than a wolf). Security says to call them if we see it...but what am I *supposed* to do with Cayotes? Play dead? Climb a tree? Don't move?
The Serre-Swan theorem strengthens the analogy "projective modules over rings are like vector bundles", prevalent in commutative algebra (and algebraic geometry).
en.wikipedia.org/wiki/Serre%E...
en.wikipedia.org/wiki/Serre%E...
Serre–Swan theorem - Wikipedia
en.wikipedia.org
October 21, 2025 at 3:36 PM
The Serre-Swan theorem strengthens the analogy "projective modules over rings are like vector bundles", prevalent in commutative algebra (and algebraic geometry).
en.wikipedia.org/wiki/Serre%E...
en.wikipedia.org/wiki/Serre%E...
I worked through one possible solution to proving Pelletier's problem 24 in the #Mizar #proofassistant, but there are others.
thmprover.wordpress.com/2025/10/19/p...
thmprover.wordpress.com/2025/10/19/p...
Pelletier’s Problem 24 in Mizar
There are probably several different ways to prove Pelletier’s Problem 24, so we will just investigate one way. Informal Roadmap for the Proof The first thing to do, whenever formalizing anyt…
thmprover.wordpress.com
October 19, 2025 at 4:59 PM
I worked through one possible solution to proving Pelletier's problem 24 in the #Mizar #proofassistant, but there are others.
thmprover.wordpress.com/2025/10/19/p...
thmprover.wordpress.com/2025/10/19/p...
Reposted by Alex Nelson
There’s a free application, shutup10++, that lets you disable all the shitty windows stuff with a series of checkboxes.
It even tracks if windows rolls anything back between updates and lets you reverse the changes with a click.
I can personally recommend shutup10++ if you need to stick with windows
It even tracks if windows rolls anything back between updates and lets you reverse the changes with a click.
I can personally recommend shutup10++ if you need to stick with windows
This is the future of Windows. Microsoft wants to rewrite Windows to turn computers into AI PCs that you talk to. It's now bringing AI features to all Windows 11 PCs today, in a bid to convince you to talk to your PC and let AI control it. Full details 👇 www.theverge.com/news/799768/...
Microsoft wants you to talk to your PC and let AI control it
Copilot Voice and Vision are now rolling out.
www.theverge.com
October 16, 2025 at 8:15 PM
There’s a free application, shutup10++, that lets you disable all the shitty windows stuff with a series of checkboxes.
It even tracks if windows rolls anything back between updates and lets you reverse the changes with a click.
I can personally recommend shutup10++ if you need to stick with windows
It even tracks if windows rolls anything back between updates and lets you reverse the changes with a click.
I can personally recommend shutup10++ if you need to stick with windows
Every time I pick up my prescription, I swing by Burrito Express to pick up the Ross Perot Burrito.
It's surprisingly good, for being named after a third party weirdo.
en.wikipedia.org/wiki/Burrito...
It's surprisingly good, for being named after a third party weirdo.
en.wikipedia.org/wiki/Burrito...
Burrito Express - Wikipedia
en.wikipedia.org
October 16, 2025 at 10:00 PM
Every time I pick up my prescription, I swing by Burrito Express to pick up the Ross Perot Burrito.
It's surprisingly good, for being named after a third party weirdo.
en.wikipedia.org/wiki/Burrito...
It's surprisingly good, for being named after a third party weirdo.
en.wikipedia.org/wiki/Burrito...
Despite the tornados and thunder storms, I wrote a brief "worked example" of how to prove one of Pelletier's problems in the #Mizar #proofassistant.
This is part of the "Mizar 101" series of posts.
thmprover.wordpress.com/2025/10/14/s...
This is part of the "Mizar 101" series of posts.
thmprover.wordpress.com/2025/10/14/s...
Schemas and Proofs: A worked example
Today, we will work through proving one of Pelletier’s Seventy Five Problems for Testing Automated Theorem Provers. The focus will be on the proof of the claim. Then we will give several R…
thmprover.wordpress.com
October 14, 2025 at 4:48 PM
Despite the tornados and thunder storms, I wrote a brief "worked example" of how to prove one of Pelletier's problems in the #Mizar #proofassistant.
This is part of the "Mizar 101" series of posts.
thmprover.wordpress.com/2025/10/14/s...
This is part of the "Mizar 101" series of posts.
thmprover.wordpress.com/2025/10/14/s...
Uh, a tornado warning *and* a thunderstorm warming has just been issued for Los Angeles...
I never lived through a "thunder tornado", but I don't think I want to...
I never lived through a "thunder tornado", but I don't think I want to...
October 14, 2025 at 3:23 PM
Uh, a tornado warning *and* a thunderstorm warming has just been issued for Los Angeles...
I never lived through a "thunder tornado", but I don't think I want to...
I never lived through a "thunder tornado", but I don't think I want to...
Microsoft has been doing this stuff for literal decades, and only now programmers are concerned about quality. I feel like I've been shouting this from the rooftops for years, and now --- only *now* --- are people concerned. The horse has left the barn...
techtrenches.substack.com/p/the-great-...
techtrenches.substack.com/p/the-great-...
The Great Software Quality Collapse: How We Normalized Catastrophe
The Apple Calculator leaked 32GB of RAM.
techtrenches.substack.com
October 14, 2025 at 3:14 PM
Microsoft has been doing this stuff for literal decades, and only now programmers are concerned about quality. I feel like I've been shouting this from the rooftops for years, and now --- only *now* --- are people concerned. The horse has left the barn...
techtrenches.substack.com/p/the-great-...
techtrenches.substack.com/p/the-great-...