Thank you for the links

Junk theorems in Lean are laughably bad due to type coercions.

Those look suspicious... I mean when you consider that the set of propositions is given a topology and an order, "The set {z : ℝ | z ≠ 0} is a continuous, non-monotone surjection." doesn't seem so ridiculous after all. Similarly the determinant of logical operations gains meaning on a boolean algebra. Zeta(1) is also by design. It does start getting juicy around "2 - 3 = +∞" and the nontransitive equality and the integer interval.

o7's already posted it! https://awful.systems/post/6746032/9903043

The flipside to that quote is that computer programs are useful tools for mathematicians. See the mersenne prime search, OEIS and its search engine, The L-function database, as well as the various python scripts and agda, rocq, lean proofs written to solve specific problems within papers. However, not everything is perfect: throwing more compute at the problem is a bad solution in general; the stereotypical python script hacked together to serve only a purpose has one-letter variable names and redundant expressions, making it hard to review. Throw in the vibe coding over it all, and that's pretty much the extent of what I mean.

I apologize if anything is confusing, I'm not great at communication. I also have yet to apply to a mathematics uni, so maybe this is all manageable in practice.

The developer of an LLM image description service for the fediverse has (temporarily?) turned it off due to concerns from a blind person.

Link to the thread in question

Good for them

Yes, they are trying to automate releases.

sidenote: I don't like how taking an approach of mediocre software engineering to mathematics is becoming more popular. Update your dependency (whose code you never read) to v0.4.5 for bug fixes! Why was it incorrect in the first place? Anyway, this blog post sets some good rules for reviewing computer proofs. The second-to-last comment tries to argue npm-ification is good actually. I can't tell if satire

Vibe coding would go just great in a theorem prover

clanker's dozen

I've never heard of a function being called entire out of complex analysis. But still, it is zero at i.

Samsung developer sends AI slop to linux mailing list

rsyslog goes "AI first", for what reason? no one knows.

Opening ipython greeted me with this: "Tip: IPython 9.0+ has hooks to integrate AI/LLM completions."

I wish open source projects would stop doing this.

Thanks for the work you do on Newgrounds! This sentence stuck out to me

No more worrying about lack of content or fickle UGC creators

Oh they're just publically advertising their company to be anti-union. Bold.

Yet another LLM guy claiming it solved a problem when in fact it was already solved, with it being told almost exactly where and what to look for. Cold reading for use-after-frees.