Claude

Hahaha Thorsten finally generated that note I was expecting him to

Huh, mathlib also only just got computable polynomials in the past couple months?...

My task today, unfortunately, is to convince ACL2 that the division and Euclidean algorithm on polynomials terminates

Never followed the Proofs and Prompts blog; crank-proximity vibe meter has not failed me yet

Unsure if already widely known but to get rid of recent annoying Firefox rounded everything UI:

about:config -> toggle browser.nova.enabled off

The problem with keeping on the bleeding edge of issues before it hits most other social media is that you get to hear your thoughts said back to you like you weren't already saying them before they went viral

Lmao John Baez has finally discovered Aella.

Wow some of these Q&A questions lmao

Listening to the Harvard webinar about the Navier--Stokes "solution" now. First point of report, dear god why are some mathematicians so namby pamby towards these fucking AI companies

"I hope that this will put an end to the worry about large AI formalization possibly abusing kernel implementation bugs"

I have questions about the huge pile of code and a mess of the proof of False-ity rejection that is formalized by AI and checked by the Lean kernel

Such uncanny valley vibes

If a computer autoformalizes a math in the forest and no one's around to understand it, does it make any sound?

Guys. You're suited to work on whatever if you stay humble and treat everyone in the same field as colleagues to help and learn from, and not competitors to beat down and denigrate. That's it.

In the meantime do feel free to follow the less spicy Professional Edition over on mathstodon.xyz (link in profile info)

Hello new follow requesters thank you for the interest though for now follows are restricted to people I have interacted with sufficiently, whether irl or online. Rest assured, hot takes based on my experiences from my younger days trying to make mathematical proof software that wasn't captured by Foreign Interests may continue

I feel like people who were not in the room when the likes of Buzzard and de Moura were doing the pooh-poohing of every single other "competitor" (their perspective) should indeed withhold judgment on the annoyingness and vindictiveness of type theorists

Nah, fuck all the way off with your juvenile ITP flame wars

BitWarden enshittification early warning: https://www.fastcompany.com/91542655/bitwarden-scrubs-always-free-and-inclusion-values-from-its-website-as-longtime-execs-step-down

Bit of a leopards-are-eating-my-face kind of vibe in a number of "AI for math" quarters going on here