This site requires JavaScript
Libera.Chat
Freenode
libera #monero-research-lounge
2 Aug 2026
Be excellent to each other.
00:54
DataHoarder
Related to formally proving incoming new methods, a soundness bug was found on Lean
leanprover/lean4 #14576
00:55
DataHoarder
some writing around it
leodemoura.github.io/blog/2026-8-1-…rtem-for-kernel-soundness-bug-14576
an hour ago
«
a day earlier
Use dark theme
Use smaller text
Don't colourise nicknames
Use wider column for nicknames
Hide IRC bots
Don't desaturate bots
Close
╳