Hacker News

Possibly pertinent: Principia Mathematica Maps and Table Site (PM-MATS): https://principia.lib.uiowa.edu/about.html - more description in my top-level comment in this page.

It seems like a frontier model LLM could probably do it in day, probably less. Someone would have to read and correct it, though

Just got this from the library, it's a real page turner. Heard about it in this excellent interview: https://www.typetheoryforall.com/episodes/goedel-s-incomplet...

Logicomix is novel, and done well, but flawed … it's deficiencies lie in what it leaves out which may come across as an unfair charge but in this case the charge is warranted. There is a more historically correct and less orthodox work waiting in the wings for whosoever should attempt it.

new comics recommendation! thanks!

It's better visually. No dot, ., :, :., ::, ::., :::, etc. have increasing visual weight, which shows which are the more top-level operators without having to match up parentheses.

This is commonly believed, but Gödel didn't identify a logical error at the heart of the whole enterprise, he proved astonishing theorems revealing limitations of any sufficiently powerful formal system. One can kind of think of the Principia as a science experiment to find the extent to which known mathematics could be proven from foundational axioms that could be thought of as "laws of logic". To make their system work, Russell and Whitehead themselves had to add extralogical axioms, such as their Axiom of Reducibility [0] and the Axiom of Infinity, giving empirical evidence (but not a proof) that "laws of logic" alone were not enough. They were also aware of limitations in their own system, such as the inability to define the cardinal $\aleph_\omega$ [1].

Like the article says, what they did was ahead-of-its-time, and a monumental influence on all subsequent work on formal systems, including Gödel's work, regardless of whether Russell and Whitehead achieved their initial aims.

[0] https://en.wikipedia.org/wiki/Axiom_of_reducibility [1] https://www.gutenberg.org/files/78255/78255-h/78255-h.htm#Pa...

Utter nonsense ... there is no known logical error in PM. Gödel proved that Russell and Whitehead's goal was unachievable but that's a totally different matter.

OTOH, Russell found a logical error at the heart of Frege's work, and PM fixed it by introducing the theory of types.

That's not how to spell Ludwig Wittgenstein!

>there is indeed a huge logical error at the heart of the whole enterprise but it was not discovered until much later by Kurt Gödel.

Which leads us to our next borderline impenetrable book, Gödel, Escher, Bach by Douglas Hofstadter.

I believe the Principia Rewrite is at https://principia-rewrite.org/.

There's a reason mathematics was known as "penalty copy" and was notoriously difficult to typeset and even more difficult to turn a profit on.

For a deep dive into both ends of that, see the history of publication of Knuth's TAoCP where the text was originally published traditionally by setting metal type on a composition machine (to the extent possible), then compositors would add the additional characters and spacing material necessary to compose the equations and so forth so as to lay out a galley (which would then be proofed/corrected) --- a successive edition was then typeset using an early imagesetter, which looked so ghastly that DEK considered giving up, but when informed that the imagesetter was controlled by a computer declared, "I am a computer scientist, I can fix that." and expected to knock out a typesetting system over his next sabbatical....

Roughly a decade later, TeX 1.0 was released.... the current version is 3.141592653 (with new versions adding another decimal place as the version tends towards \pi) --- while we're still waiting on the full publication of Vol. 4, it is widely considered that TeX was worth the delay.

apocryphally a typesetter saw "make x as small as possible" at the end of a math problem to be typeset, and did exactly that

You might be thinking of Russell's Principles of Mathematics which is a bit easier going.

No it's not.

No it wasn't.

And you did not read it.

EDIT: source: took logic as undergrad + wrote on the tractatus which required a lot of pre-reqs to understand. 0 chance a course at undergrad level ever assigns principia mathematica. I don't care if you went to yale or oxford or ecole normale ... 0 chance. Most charitable interepretation: some pages of it + was on a bibliography. not required reading.

if feel embarrassed, that is the consequence for lieing. There is such a thing as intellectual honesty.

link the syllabi for the classes

It is not. The foundation of math is contested -- but afaik it is widely held that HoTT is the, erm, hottest contender to the throne https://en.wikipedia.org/wiki/Homotopy_type_theory

Oops wrong principia :-)

I would highly recommend "PROGRAM = PROOF" by Samuel Mimram.

It covers everything from pure lambda calculus through dependent type theory up to homotopy type theory. In comparison to the HoTT book, the book "PROGRAM = PROOF" is oriented less towards mathematicians more towards programmers. It contains also a short introduction to OCaml and Agda.

The book can downloaded from the authors web page:

https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...

https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/publicat...

This is probably a reasonable example of a case where an AI can really help out as an endlessly patient assistant to answer your personal questions in a conversational format.

It is possible it may get something wrong but as long as you keep beating on the wrongness you should eventually be able to work out what it is, and in its own way that would become possibly the best learning exercise there is. And of course, with the math proofs coming through from AIs lately, I wouldn't guarantee you'll see that much wrong stuff. I expect it would be at a low enough rate to keep you learning... after all, anyone who has had serious math education knows the human teachers aren't always completely correct either and there is the occasional impromptu exercise of everyone staring at the board and trying to figure out what went wrong with the demonstration.

> I am interested in different approach to types, using triage calculus, which is more "materialist" than "structuralist" - type is given by the structure of the (quoted) term in normal form (unlike lambda calculus, triage calculus makes quoting easy).

Interesting, dropping this link here for others: https://treecalcul.us/

HoTT distinguishes equality from equivalence.

Univalence says that equality is equivalent to equivalence, ie, formalizing the notion of when we can use equivalence rather than equality as a step in a proof. In practice, we often only care about proofs “up to equivalence”.

A way to think about this:

- equality is an identity map

- equivalence is an isomorphism

For example, 2 in Z and 2 in R do not have an identity map between them — but do have an isomorphism.

I think the key insight of univalence is not collapsing equivalence into equality — but allowing it to remain a second truth relation.

We don’t want 2 in Z to be equal to 2 in R (because we collapse type distinction), but we do want them to be equivalent — so we can do equivalent reasoning about arithmetic in R to reach conclusions about Z.

David Spivak (no relation to Calculus Spivak) wrote a book called _Category Theory for the Sciences_ that could totally serve as the basis for a one-semester undergrad course with some work.

He really likes working in informal categories (like his “ologs”) but I haven’t taught from it yet so I’m not sure if it is more or less confusing to introduce categories that way.

Yikes, guys/girls. I got downvoted to -4 points for a misunderstanding or something. Because the author of the website would probably agree with my simple point that although the Principia Mathematica tried to do the impossible, there is still utility for its value as a programming self-teaching resource for serious students of computer science.

Wow. Yeah. You guys ironically didn't just throw out the baby with the bath water thing. You burned me at the stake like a witch for heresy. Due to your cognitive biases and distortions.

You guys are Imperium of Mankind coded or something?

>Again, I think this is a programmer centric way of looking at things: “how do I know it’s right if I can’t compile it”.

I would argue this would only be true for those without formal education. Writing your code on paper is very common in CS courses. You get used to not being able to compile it.

I think your latter comment is kind of analogous to people writing python (or any high-level language) without understanding assembly. I think maybe that reduces the mystery a bit?