Pinned toot

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.

To top it all off, this is most likely gonna go into an appendix, never to be seen again.

Checking this by hand would've taken me much longer because I would first have to read and understand all of the proofs again.

So I had these results about a system (from a project from last summer actually, what is time?) but I needed to change some of the definitions to have a chance at publishing them. Fortunately, I formalized everything in Coq, so this evening, I adjusted the definitions and all proofs went through (with minor modifications). Thank you Coq and thank you past me!

- 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