← Feed

Posts

• Post #4301117

  RE: https://mathstodon.xyz/@danielgratzer/117003175661766753 We are working together in Daniel’s office, and every time his computer dings with another like on this post, he looks at me like 😏

• Post #4301116

  In a previous wave of Lean discourse, there was discussion about the fact that type-checking a Lean file can run arbitrary code. There are pros and cons to this, but one particularly obvious con is, well, let's just hear Kevin Buzzard's version: "One cannot trust AI-generated code so I ran [the AI-generated formalization of the Erdős unit distance conjecture counterexample] in a sandbox on my machine (malicious Lean code can run arbitrary commands on your computer — Lea...

• Post #1889743

  Went to lunch today with the PL grad students, who started discussing their relatively large range of ages. Student 1: Well, I'm 24. Me: I mean, isn't that the age Coolio said he wasn't sure if he'd live to see? Student 2: Who's Coolio? Student 3: That's a musical artist, right? Student 2: ...from the 1900s? [@samth and I are dying]

• Post #1863936

  PCF is a domain-specific language for ω-cppos.

• Post #1471256

  17th century mathematical mistakes: I have a proof that is too large to fit in this margin. 21st century mathematical mistakes: I have a file that is too large to fit in this buffer.

• Post #1467645

  Does anybody here have any opinions about the candidates in the ACM general election, vis-à-vis the Digital Library, ACM financials, or other hot-button issues?

• Post #1330076

  LICS paper with @trebor accepted! 🎉

• Post #661144

  I had totally forgotten about this slide deck about gluing from years ago...

• Post #351369

  Here's what I've learned about generating accessible PDFs with LaTeX! ...especially for any American academics at public universities whose materials need to meet accessibility requirements starting April 24, 2026. :) https://www.carloangiuli.com/pages/accessible-latex.html