@lipsum.dev on Bluesky

Post

Thomas🪴

lipsum.dev

did:plc:denld7ao24tcahogbclo3if3

Avec l'assistant de preuve Lean : theorem married_looks_unmarried (H1 : Looks Paul Linda) (H2 : Looks Linda John) (H3 : Married Paul) (H4 : ¬Married John) : ∃ x y : Person, Married x ∧ ¬Married y ∧ Looks x y := by by_cases h : Married Linda · exists Linda, John · exists Paul, Linda

2025-10-29T16:18:37.857Z

Enable JavaScript to use Bluesky.

Learn more about Bluesky at bsky.social and atproto.com.