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.
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-...
For the first time in months, it is raining. Quite heavily, too.
Thank goodness I don't have to go to class today, I'd hate to run 5k in this weather, and wait for buses...
Thank goodness I don't have to go to class today, I'd hate to run 5k in this weather, and wait for buses...
October 14, 2025 at 2:28 PM
For the first time in months, it is raining. Quite heavily, too.
Thank goodness I don't have to go to class today, I'd hate to run 5k in this weather, and wait for buses...
Thank goodness I don't have to go to class today, I'd hate to run 5k in this weather, and wait for buses...
I write a little fiction, nothing serious...because I realize there's a huge canon I have to work my way through, full of amazing writers like Jane Austen.
I couldn't imagine a [fiction] writer admitting out loud to have not read Jane Austen, and not realizing they were missing out on it.
I couldn't imagine a [fiction] writer admitting out loud to have not read Jane Austen, and not realizing they were missing out on it.
I did an mfa in fiction writing with a lot of men who had never read Jane Austen and weren’t even embarrassed about that and I had no respect for them
Tell me your most unhinged literary opinion, as a little treat
October 14, 2025 at 12:46 AM
I write a little fiction, nothing serious...because I realize there's a huge canon I have to work my way through, full of amazing writers like Jane Austen.
I couldn't imagine a [fiction] writer admitting out loud to have not read Jane Austen, and not realizing they were missing out on it.
I couldn't imagine a [fiction] writer admitting out loud to have not read Jane Austen, and not realizing they were missing out on it.
I'm not convinced Aschbacher's definition of a "building" generalizes Bourbaki's definition, but it's built on so many layers of abstraction it's hard to keep track of things 😂
October 12, 2025 at 12:37 AM
I'm not convinced Aschbacher's definition of a "building" generalizes Bourbaki's definition, but it's built on so many layers of abstraction it's hard to keep track of things 😂