Lightnews — Scholar-powered news

Alex Nelson @pqnelson.bsky.social · 18h

Well, I guess the alternative to "living through" a thunder tornado is "dying in a" thunder tornado, which seems even less appealing...

Alex Nelson @pqnelson.bsky.social · 18h

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...

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 &#82…

thmprover.wordpress.com

Alex Nelson @pqnelson.bsky.social · 20h

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...

1 1

Alex Nelson @pqnelson.bsky.social · 20h

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-...

The Great Software Quality Collapse: How We Normalized Catastrophe

The Apple Calculator leaked 32GB of RAM.

techtrenches.substack.com

Alex Nelson @pqnelson.bsky.social · 21h

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...

Alex Nelson @pqnelson.bsky.social · 1d

Read later, kinda interesting "dialect" of literate programming...

arxiv.org/abs/2510.09073

Literate Tracing

As computer systems grow ever larger and more complex, a crucial task in software development is for one person (the system expert) to communicate to another (the system novice) how a certain program ...

arxiv.org

Alex Nelson @pqnelson.bsky.social · 1d

It's like a chef who doesn't know how to use a frying pan and a stove top. Like, what are you even doing?

Alex Nelson @pqnelson.bsky.social · 1d

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.

Julia Carrie Wong @joolia.bsky.social · 1d

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

Rachel Feder @rachelfeder.bsky.social · 1d

Tell me your most unhinged literary opinion, as a little treat

1

Alex Nelson @pqnelson.bsky.social · 3d

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 😂

Alex Nelson @pqnelson.bsky.social · 3d

Yeah, I think that's probably a good suggestion (to do some ZFC formalized in Mizar). I'm going to need to do a few preliminary stuff first, because formalizing even a basic result in set theory in Mizar assumes quite a bit of material I have not yet covered. Well, at least a couple blog posts...

Alex Nelson @pqnelson.bsky.social · 3d

I've started a "Mizar 101" series of posts oriented towards people who have just installed the #Mizar #proofassistant, but don't really know what to do from there.

The first thing to check is that you installed Mizar correctly, that it "works".

thmprover.wordpress.com/2025/10/11/h...

How to check you installed Mizar correctly

We will be starting a “Mizar 101” series of posts, which will focus on “first steps in Mizar”. This post will discuss, among other things, “How to check you installed …

thmprover.wordpress.com

Alex Nelson @pqnelson.bsky.social · 4d

I mean, Omnibus 6 is the last one, so if I don't find out there, then it's impossible to find out what happened 😢

Alex Nelson @pqnelson.bsky.social · 4d

So I finished Gotrek & Felix Omnibus 4 wondering if Snorri ends up getting to the shrine of [dwarf god] and [event happening].

Then Omnibus 5 begins anachronistically between the first and second book.

But...but...what happens to Snorri Nosebiter? Maybe I'll find out in Omnibus 6...

1

Alex Nelson @pqnelson.bsky.social · 4d

Also might be interesting (for finite group theory stuff):

arxiv.org/abs/2510.08426

On the $IC$-$Π$-property of subgroups of finite groups

Let $ H $ be a subgroup of a finite group $ G $. We say that $ H $ satisfies the $ Π$-property in $ G $ if $ | G/K : N_{G/K}((H \cap L)K/K)| $ is a $ π(( H \cap L)K/K ) $-number for any chief factor $...

arxiv.org

Alex Nelson @pqnelson.bsky.social · 4d

Read later

arxiv.org/abs/2510.07851

The Functional Machine Calculus III: Control

The Functional Machine Calculus (Heijltjes 2022) is a new approach to unifying the imperative and functional programming paradigms. It extends the lambda-calculus, preserving the key features of confl...

arxiv.org

1

Alex Nelson @pqnelson.bsky.social · 5d

OK, I was told my blog posts on Mizar are not simple enough for beginners, so I will start a "Mizar 101" series of blog posts which will work through even simpler material.

...I just need to think of even simpler material to write about...

1 1

Alex Nelson @pqnelson.bsky.social · 7d

I'm surprised to hear you're surprised, but I was under the impression this is common knowledge among type theorists. So perhaps I am mistaken about how prevalent "pre-syntax" is among proof assistant people.

1

Alex Nelson @pqnelson.bsky.social · 12d

It appears everyone credits Hoffman's "Syntax and Semantics of Dependent Types" (1996?) with inventing presyntax, as a way to give a semantics using untyped computation.

Alex Nelson @pqnelson.bsky.social · 12d

TIL about the Lindamood Bell theory of reading, where the reader uses visualization to read each word instead of trying to pronounce each phoneme.

Apparently, this helps a lot of people with dyslexia read stuff better (or, in some cases, at all).

Alex Nelson @pqnelson.bsky.social · 14d

What's the origin story of "preterms" and "pretypes" in type theory? I never got a clear history of the notions, and they seem pretty important even in simply typed lambda-calculus.

2

Alex Nelson @pqnelson.bsky.social · 15d

I just found out the paper I'm a co-author on, got posted to the arXiv yesterday.

Neat.

José A. Alonso @jalonso.bsky.social · 15d

Composition direction of Seymour’s theorem for regular matroids — formally verified. ~ Martin Dvorak et als. arxiv.org/abs/2509.20539 #ITP #LeanProver

Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified

Seymour's decomposition theorem is a hallmark result in matroid theory presenting a structural characterization of the class of regular matroids. Formalization of matroid theory faces many challenges,...

arxiv.org

1

Alex Nelson @pqnelson.bsky.social · 16d

Good grief, I am tired. I just returned home after visiting family for about a week.

Tomorrow I need to get up at 5am, to catch a bus at 5:30am to take me to Caltech by 7am. Then I return home catching a bus at 3:45pm at Caltech, and I should get home around 4:45pm.

1

Alex Nelson @pqnelson.bsky.social · 23d

I'll be out of town visiting my grandparents for a week, so if you want to tell me my political opinions are stupid, you have until tomorrow...

Alex Nelson @pqnelson.bsky.social · 24d

The only work on "schemas" in logic seems to be Corcoran's "Schemata: the Concept of Schema in the History of Logic".

Is there anything more substantial than the lip-service of "Schemes are formulas with metavariables"?

1 2

Alex Nelson @pqnelson.bsky.social · 25d

Yeah, I realize that TeX is a "sacred language" to me, and I am perfectly happy with that.

1 1