Jons Mostovojs @jonn@social.doma.dev

@jonn see the second link ;)

PSA, if someone asks you for contact info (e.g. a phone number) of someone you know, the correct response is "I can't give that to you, but I can give them yours".

It's efficient and adds no round-trips, it's privacy friendly, it's non-awkward and it's social engineering resistant. It's a universally good rule.

And the corollary, of course: Don't ask someone for another person's contact info - ask them to pass on yours.

Everyone: the racist, sexist, violent system has failed us

Tech bros: idk, it works on my machine

Added my inks to the print shop! Shipping is free the whole weekend too! https://www.inprnt.com/gallery/allisonchinart/

The New York Times has a profile by Siobhan Roberts on the Online Encyclopedia of Integer Sequences, celebrating its 50th anniversary: https://www.nytimes.com/2023/05/21/science/math-puzzles-integer-sequences.html, https://web.archive.org/web/20230522005810/https://www.nytimes.com/2023/05/21/science/math-puzzles-integer-sequences.html

Worthwhile reminder for all you designer types out there

Cleaning your space is self care, too.

Tomorrow I'm off to Canada (Banff) for a week, to work on cohomology theories in Lean. Adam Topaz is one of the organisers of the conference, and he whetted our appetite earlier this week by writing down the definition of singular homology:

```
def integral_singular_homology (n : ℕ) : Top.{0} ⥤ Module ℤ :=
Top.to_sSet ⋙ ((simplicial_object.whiskering _ _).obj (Module.free ℤ)) ⋙
algebraic_topology.alternating_face_map_complex _ ⋙ homology_functor _ _ n
```

In fact this definition has been kicking around for a while -- Brendan Seamas Murphy used it here https://github.com/Shamrock-Frost/BrouwerFixedPoint/blob/52f48d25068df0eadf3df5b2ede7bcb087d30527/src/brouwer_fixed_point.lean#L274 eight months ago in his proof of the Brouwer fixed point theorem. It's all well and good making enough definitions in category theory to give a cool looking definition of the homology of a topological space; the big testing ground in formalisation is not "can you define the object", it's "can you actually prove some theorems about your definition"? A lousy definition might be unusable in practice. Brendan proved for example here https://github.com/Shamrock-Frost/BrouwerFixedPoint/blob/52f48d25068df0eadf3df5b2ede7bcb087d30527/src/homology_of_spheres.lean#L2043-L2045 that $H_n(S^n,R)$ was isomorphic to $R$, for $R$ a nonzero commutative ring.

My PhD student Amelia Livingston has done the same thing for group cohomology; her definition has hit Lean's maths library, which means that it will live for as long as Lean lives. It's here https://leanprover-community.github.io/mathlib_docs/representation_theory/group_cohomology/basic.html . Amelia has further work proving things like Inf-Res, Hilbert 90 and so on, proving that her definition is usable.

After next week it will be interesting to see how much more progress we have made with cohomology theories. Topological K-theory is close, and another target for this week is etale and proetale cohomology of schemes. Wish us luck in the mountains of Canada!