treppenverstand @treppenverstand@types.pl

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.

Turns out people *have* been doing stuff similar to what I am doing.

Relearning a lesson I should've already learned from my Bachelor's thesis: I should've done my literature review earlier!

Attended a really cool talk today which makes up for all of the subpar one of the past 2 weeks.

Didn't even finish that proof today. I'll probably have to work over the weekend now :./

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

I cannot fathom how people doing pure category theory or algebra enjoy this stuff. This is pure torture to me.

I've spent like 2 hours today on (what feels like, to me) pure category theory and I hate it. Is this the price you pay for nice definitions?

LRT: This is what applied category theory sounds like to me.

Fuck overleaf tbh

I'm looking for a template/document style for a pretty thesis. I don't need a title page (the institute provides that) just nice styling for the actual content.

Today is my first day of thesis writing.. Let us see how it goes, both fun-wise and pages-per-day-wise...

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!