Zulip Chat Archive
Stream: mathlib4
Topic: !4#3206
Jeremy Tan (Mar 31 2023 at 16:03):
!4#3206 try and fix the remaining errors over here on April Fools' Day. (Traditionally I abstain from most of the Internet on that day, since the jokes are unfunny)
Jeremy Tan (Mar 31 2023 at 17:50):
(deleted)
Jeremy Tan (Mar 31 2023 at 17:50):
(deleted)
Last updated: May 02 2025 at 03:31 UTC