lyxia @lyxia@mamot.fr

I love math so much, I'd become a historian, so I can date theorems.

"Dating a mathematical concept is almost always a challenge"

https://m-cacm.acm.org/magazines/2022/1/257448-fifty-years-of-p-vs-np-and-the-possibility-of-the-impossible/fulltext

❤️❤️❤️ but it's so worth it.

Blogpost, on proving lists infinite in #Coq

https://blog.poisson.chat/posts/2021-10-26-proving-lists-infinite.html

I wrote about a proof by parametricity in Coq
https://blog.poisson.chat/posts/2021-10-20-initial-final-free-monad.html

I wonder whether I can turn my US vaccine certificate into a FR vaccine pass.

Writing tools I learned from The Economist

https://builtbywords.substack.com/p/writing-tools-i-learned-from-the

What if nothing is real and everything is an abstraction

What is a type?

My personal take: https://blog.poisson.chat/posts/2021-03-17-what-is-a-type.html

Fun #coq challenge by Talia Ringer on twitter:

How fast can you prove

N.succ (N.add x y) = N.add x (N.succ y)

without stdlib lemmas? As in, pretend you only just defined N and its operations.

NB: this is the binary N, not the unary nat, so it's a bit trickier than it looks.

(The starting import is "From Coq Require Import NArith.")

- I was born on a year of the Rooster
- I learned Coq on a year of the Rooster

🤔

"The one person we've found in every CLIP model is Donald Trump."

via @liaizon

https://social.wake.st/@liaizon/105834345780232950

@liaizon
This paper explains it in a very interesting way too! With plenty of data supporting the idea of neurons which respond to concepts however they appear.

I made some slides on trying to understand equality https://docs.google.com/presentation/d/1Z1i38i4_mtW11_0KmbYz1o2SwjtlaWHB1j_cZyQ0Mr4/edit

Ancient egyptians worshipped cats, because cats inspire awwe.

Can we say that functions in cubical type theory are CuTT Pi's?