Pinned toot

Driven out of Cantor's paradise and thrown into setoid hell.

Pinned toot

I do math because it means I need to do less annoying garbage than when programming. I do Proof Theory because I'm still an annoying garbage doer at heart.

Pinned toot

Here's the quote justifying my weird username. It's from Dedekind's "Was sind und was sollen die Zahlen" ("What are numbers and what are they good for?").

"But I know that, in the shadowy forms which I bring before him, many a reader will scarcely recognize his numbers which all his life long have accompanied him as faithful and familiar friends; he will be frightened by the long series of simple inferences corresponding to our step-by-step understanding [ger. Treppenverstand], by the matter-of-fact dissection of the chains of reasoning on which the laws of numbers depend [...]"

The term thus characterizes our capability of reasoning to be restricted to discrete steps and is meant to contrast the rather informal, intuition-based proofs that were the norm back in 1888 when the paper was written.

It is also a very funny sounding word.

But just spelling this out already makes it clear that that's *way* too good to be true. At least it's nice to know that all the recursive ordinals I need to care about are path's through Kleene's O...

Show thread

Sadly, the proof is not effective. It would slap if I could just pass decidable well-ordering to some function and it would compute me a Kleene ordinal coding of the order type.

Show thread

Always super cool when a surprising fact has a simple proof. Today: Every recursive ordinal has a code in Kleene's O.

When a paper is so old it needs to explain what "recursive" (in the sense of mu-recursive) means. :floshd:

:cannabis:​ 

they should serve edibles at conferences

All spaces/content around/for PhD students are full of negativity (stress, impostor syndrome, depression, loneliness). Kinda fucked up that it is so hard to enjoy this. At least from what I have gleamed from historical stuff, it wasn't always like that.

Erratum: looking at my source (logicomix), Hilbert said "In mathemathics, there is no ignorabimus", meaning there is no "we shall not know". Leibniz says calculemus.

Show thread

The modern computerized-proof world is such a delicious mashup of the arch-rivals Hilbert and Poincare.

Hilbert had a grand dream that when two people disagreed, they could just say "calculamebus" (let us calculate), yet this was married to the "analytic" viewpoint of set theory. Poincare had a disdain for logic, and yet still championed a "synthetic" viewpoint that was key for the development of constructive mathematics!

The modern proof assistant owes a debt to both.

Maybe I should start collecting nice quotes? Could be cool to have handy.

There seems to be a fascinating connection between mathematics and environmental activism. There ought to be some writing on this...

@ionchy well, I think the idea isn't that what we find is absolute truth but rather that there is some abstract absolute truth. think of the sense of wonder you first experienced when discovering curry-howard, connections between seemingly unrelated areas. isn't it compelling to think that there is some higher abstract form of mathematical truth which escapes us and our models? I don't think like this myself, but I am tempted to every now and then..

Grothendieck revolutionized mathematics. Then he disappeared. He became a hermit, living in a stone hut and taking a vow of silence.

There's a great story about him here. And a conference about him next week!

(1/n)

newyorker.com/magazine/2022/05

I have been convinced to give the presentation. I just hope they won't be mean to my face about it!

Show thread

I've been offered to present something at a workshop in a few weeks. But it is organized by the person who gave our last paper such a scathing review. So now I'm sort of scared...

which use of torrents is worse for society?

RT @blackpooltower
Love this Le Guin quote in @jamesbridle fascinating new book, which explores “an ecology of technology”

(cc @CarbonCycleKate )

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.