Pinned toot

#introductions 

An introductions post, since I've got a bunch of new followers in the last couple of weeks (hello everybody!)

By day, I do computer verification of in the Lean prover, by night I do . When there isn't a plague going around, I like in nature and befriending . I also know a bit of .

I really like explaining concepts — feel free to ask any question (esp. mathematics / theoretical comp sci). Replies to toots are always welcome.

Pinned toot

(of course, my gender is just a temporary situation until my Glorious Lisp OS-powered Robot Body finally is usable in daily life!)

Show thread
Pinned toot

ME, ONE YEAR AGO: this mexican party is good, but it has... how can one say ... too many people? there are in fact, only so many people one can dance with in the course of a party. I think I'm right in saying that, aren't I?

MY WIFE: this is absurd!

ME: my dear, don't take it too hard. it's quality celebrating. there are simply too many people. just remove a few, and it will be perfect.

MY WIFE: which few did you have in mind?

Pinned toot
Pinned toot

we are rebranding crypto. it no longer means "security math" or "scammer math," now it exclusively refers to people and things that crawl out of crypts.

i dont want to hear about your crypto unless you were recently sleeping underground in a cemetery.

sorry bigfoot lovers, your use of crypto is also banned. zombies only!

daily AoC (axiom of choice), day 7 

Here's a statement I didn't know was equivalent to the axiom of choice one week ago:

For all infinite sets A, the cartesian product A × A is in bijection with A.

(Hint: show that this implies the well-ordering principle.)

Show thread

update: i managed to power through. worried that my face will permanently stay as 😬 though.

Show thread

made my tea too strong. currently alternating sips from my tea with sips from a cup of hot water.

send help

it kinda bugs me more than it should when ppl are like "lol computers are made of sand"

... because that doesn't come close to how actually weird it really is.

this is the crystal (literally one single atomic crystal) that chips are sliced from like fucking magical deli ham

it was grown, by people, from a seed crystal mined from the earth, through a FUCKING MAGICAL POTION LETS JUST BE HONEST OKAY

so i was wondering what the #hitomezashi pattern with a #thueMorse sequence (used horizontally and vertically) looks like. so here you go 😃!

it's mildly trippy and definitely thue-morse-y.

it's made by hand in inkspace, but i should probably code it to try more variations…

In this episode of Star Trek, Picard plays the role of the Vichy government. Again.

Show thread

In this episode of Star Trek, the crew of the Enterprise meets Cardassian leader Gul Ibble

@Dee I don't fit within the non-binary nonbinary binary.

making a gender selector where the two options are "non-binary" and "nonbinary"

are you a statistics enby (i.e. mean(man,woman)) a quantum mechanical enby (i.e. superposition of |man> + |woman> and can change when observed) or a linear algebra enby where you are mearly projected onto the [man,woman] spectrum but cannot be fully described in fewer dimensions?

Fun fact: Phi (~1.618) is really close to the ratio between miles and kilometers (~1.609), which means you can use adjacent fibonacci numbers to quickly mentally convert back and forth between them.

for instance: 21 kilometers is roughly 13 miles (it's actually 13.05)

daily AoC (axiom of choice), day 6 

Let's get the other famous equivalent out of the way: the well-ordering principle states that every set can be well-ordered.

More precisely, for any set S there exists a function min : P(S) \ {∅} → S such that:
* min X ∈ X
* min (Y ∪ {min X}) = min X for Y ⊆ X
* if min {x, y} = x and min {y, z} = y, then min {x, z} = x

DO-TIP: prove that defining x ≤ y as "min {x, y} = x" gives a linear order and min returns the minimum of each set according to this order.

Show thread

lb: sometimes a family can be a middle aged couple and their three pasta cats

Show older
Vachtnoes

Mastodon is a server for a federated social network: everyone can run a server if they want to, including me. So this is a Mastodon server for me (Vierkantor) and my friends.