pounce :verified_blobcat: boosted
pounce :verified_blobcat: boosted

You've got to understand how much the politicians are into AI. They have so much in common. They're both dangerously full of shit and they aim to marginalise people who notice.

im done trying to get this mathlib commit to build on my laptop with 16gb of ram
i'll just let it build on a GH runner instead

i need to learn how to read mathematical french

i should just unsubscribe from the haskell café mailing list, i literally just throw all of the emails into the bin

one of these days imma write a cubical type checker for lean just you wait
and then nobody can tell me to use agda

pounce :verified_blobcat: boosted

to tired to keep filling proof holes
bed time :dragnblanketsleep:

ok time to try to formalize the sheaf of relative kähler differentials in :lean:

oh shit why did nobody ever tell me the □ modality can be used to represent local properties in the internal language of a sheaf topos that's poggers

lets see if i can learn topos theory in one day :dragnowo:

wayland stop putting all of your protocol extensions in xdg-desktop-portal challenge

zulip compile without modifying my ~/.npmrc challenge

pounce's new term for algebraic geometry: "sheaf math"*

*also applies to: algebraic topology, differential geometry, category theory.....

Show thread

dang now im wishing i were doing sheaf math in cubical agda instead of lean

Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.