20
https://github.com/leanprover/lean4/blob/master/.claude/CLAUDE.md
Imagine if you had to tell people "now remember to actually look at the code before changing it." -- but I'm sure LLMs will replace us any day now.
Also lol this sounds frustrating:
Update prompting when the user is frustrated: If the user expresses frustration with you, stop and ask them to help update this .claude/CLAUDE.md file with missing guidance.
Edit: I might be misreading this but is this signs of someone working on an LLM driven release process? https://github.com/leanprover/lean4/blob/master/.claude/commands/release.md ??
Important Notes: NEVER merge PRs autonomously - always wait for the user to merge PRs themselves
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
I don’t like how taking an approach of mediocre software engineering to mathematics is becoming more popular
would you be willing to elaborate on this? i am just curious because i took the opposite approach (started as a mathematician now i write bad python scripts)
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.
no need to apologize, i understand what you mean. my experience with mathematicians has been that this is really common. even the theoretical computer scientists (the "lemma, theorem, proof" kind) i have met do this kind of bullshit when they finally decide to write a line of code. hell, their pseudocode is often baffling
if you are literally unable to run the code through a machine, maybe focus on how it comes across to a human reader? nah, it's more important that i believe it is technically correct and that no one else is able to verify it.
load more comments
(4 replies)
load more comments
(9 replies)
From the new Yann LeCunn interview https://www.ft.com/content/e3c4c2f6-4ea7-4adf-b945-e58495f836c2
Meta made headlines for trying to poach elite researchers from competitors with offers of $100mn sign-on bonuses. “The future will say whether that was a good idea or not,” LeCun says, deadpan.
LeCun calls Wang, who was hired to lead the organisation, “young” and “inexperienced”.
“He learns fast, he knows what he doesn’t know . . . There’s no experience with research or how you practise research, how you do it. Or what would be attractive or repulsive to a researcher.”
Wang also became LeCun’s manager. I ask LeCun how he felt about this shift in hierarchy. He initially brushes it off, saying he’s used to working with young people. “The average age of a Facebook engineer at the time was 27. I was twice the age of the average engineer.”
But those 27-year-olds weren’t telling him what to do, I point out.
“Alex [Wang] isn’t telling me what to do either,” he says. “You don’t tell a researcher what to do. You certainly don’t tell a researcher like me what to do.”
OR, maybe nobody /has/ to tell a researcher what to do, especially one like him, if they've already internalized the ideology of their masters.
good morning awful, I found you the first thing you’ll want to scream at today
palantir and others offering free addictions, all in the name of “productivity”
load more comments
(6 replies)
Foz Meadows brings a lengthy and merciless sneer straight from the heart, aptly-titled "Against AI"
When you go so hard you Hadamard
OT: Did you guys know they give cats mirtazapine as an appetite stimulant? (My guy is recovering from pneumonia and hasn’t been eating, so I’m really hoping this works).
Rooting for your kitty!
load more comments
(2 replies)
load more comments
(1 replies)
this post was submitted on 29 Dec 2025
20 points (100.0% liked)
TechTakes
2722 readers
251 users here now
Big brain tech dude got yet another clueless take over at HackerNews etc? Here's the place to vent. Orange site, VC foolishness, all welcome.
This is not debate club. Unless it’s amusing debate.
For actually-good tech, you want our NotAwfulTech community
founded 3 years ago
MODERATORS