treppenverstand @treppenverstand@types.pl

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

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.

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.

Organizing Proof and Computation in Fischbachau is dangerous. I've ended up skipping a bunch of sessions to go on hikes so far and there is no sign of this stopping...

Proof and Computation is so much more fun than WoLLIC. Not only are we in the alps (very cool!), there's also tons of super interesting discussions going on around me. If I can just internalize 15% of that, I will have learned soooooo much!

I'm at the Proof and Computation autumn school now and surprisingly, the courses I enjoy the most so far were the ones I thought the lowest of from looking at the program.

Do conferences involve lots and lots of drinking for everyone or is that just me?

Conference dinners rock!

On a conference all alone and it is *scary*. Sleeping alone in the forest at night has nothing on this lol.

conclusion
bottom sequent

Why do authors always insist of awful notation?

I wish people would stop saying stuff like "the set X is recursive" and instead say "X is in Sigma_1". But that's probably super taste dependent.

If type theory is so bad, where's the L-type?

I'm barely halfway through creating the presentation and already at 20 slides! I only have 1 hour for my talk so it might get tight!

Also, it seems if I don't have to fight TeX my layouts get pretty unhinged. Not sure how easy this will be to follow...

Like, drawing pictures is *much* faster than tikzing but writing is also much slower than typing. The idea was to have many pictures and little text, so maybe it will work out?

Trying out hand-drawn slides for my next talk. Not yet sure of they're more efficient to create...