Viewing profile — lakesare

Loving the sepia theme, and in general fells really pleasant to me (something I did lack in other writing software). I think I will try it for my next project :)

I have non-24-hour sleep disorder with a 25-hour cycle, and used to draw these calendars manually in Excel to track my shifting sleep schedule. Finally automated it. Green cells sh…

Thanks for the link. I've been reading Leslie Lamport's TLA works this year coincidentally, but never stumbled upon this one. His structured proofs would turn into a paperproof-sty…

Reminds me of characteristica universalis

I love "Lean" actually, have you noticed ∃∀. Googling Lean concepts does primarily return the codeine syrup links though yes.

That's correct, in fact we would have a DAG if we displayed all possible arrows, but we conceal it to make the UI easier to interact with for the user. Hypotheses (green nodes) for…

It isn't necessary to know theory for these visualisations to be useful, both Traf and Paperproof (and sequence calculus trees!) should, ideally, just reflect what's already happen…

This is my overview of proof visualisation tools among all modern proof assistants. If you're aware of any tools I might have missed, please @ me in the comments. I aimed to cover …

A blog post where I catalog all Lean [proof assistant] books that exist in nature, share my opinion on them, and suggest learning paths for Lean novices.

It does violate the perfect "Cartesian coordinates" normalization I described earlier, however I consider this is a permissible step up over the full normalization, because, while …

Hah, it basically goes into denormalisation! This certainly looks prettier than the initially shown full-fledged table structure, however I'm having more trouble reading it - it ma…