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.

Haha, simply compute the bound of the depth of the reduction tree. Surely that can't be that hard...

Show thread

in other maths u have to explain ur proofs to the reader who can think, but agda is brain empty

Actually, I can constructivize parts of it. Probably enough to get the things I actually care about to be constructive...

- pronouns
- he/him/his

- age
- early 20s

- academic level
- master's student

studying mathematical logic • ex-CS student • interested in type theory + constructive mathematics + game semantics + non-economic games • will only write code that doubles as proof

trans rights + against all unjust hierarchies

Joined Oct 2020