It's always fun to see the people throwing fits over this kind of thing. No matter what approach/wording they use, and no matter how hard I try to give them the benefit of the doubt, the mental images my mind forms of these people is always entertaining.
Ofc, it's less fun to accept that many of them are probably bots, but whatever.
Honestly I think I'd have an easier time understanding 1000s of lines of slop than 93 lines of proofs lol.
Does anyone have any recommended learning resources for this type of thing? Skimming the repo, it looks like a lot of unicode and math terminology, but this project seems really compelling to me.
I learned working with the Isabelle proof assistant in a university course. There were weekly exercises and a group project at the end. (Actually proving things by hand, no LLM.) That really helped. Before that course it was also hard for me to get into this.
Other than that you can also read introductory material for set theory. There the meaning of all of the unicode symbols you can see in the spec should be explained.
This would probably be more effective (and controversial) if the reports included the linkedin profiles of the recruiters/employees involved in the ghosting.
I can imagine a lot of situations where it'd be unfair, so maybe giving them an opportunity to explain their side before it goes up might be important... but also fuck you if you ghost someone trying to find a job.
1. The AI they used called it "physics-based" as a hallucination (probably due to the popular "JellyCar" game), and they went with it because they don't know better.
2. They don't know better, so they asked the AI for a "physics based" system, and the AI was too sycophantic to correct them.
I see the growing trend of words losing all meaning is still going strong in 2026. I wonder what human communication will look like in the near future?
Yep, it's very weird. Consumed, listened to... There's ways to say the thing like it is. I guess "read" carries a certain superior connotation so people lean on it.
Note that I do think reading is superior. This is not to diminish anyone who chooses to listen to books. Some people do it because of accessibility, some because of time (can listen while commuting, or in the gym), or they just choose to listen to some books they don't care as much whilst still read the ones they do.
This is all great and people should be encouraged to do what works for them - but please don't pretend it's the same. Sometimes I even think we need a different word for reading e-books.
So you're saying that it's not fair to rate a coding model on its ability to code, and instead the best way to use it is to tell it to find existing human-written code online rather than generate actual code on its own?
If you're testing how good LLMs are at compressing information, then I think that's a fair test. Personally, I don't really think that's where their strength comes from (especially considering how much more useful local models that are orders of magnitude smaller than Claude/OpenAI-tier models have gotten). In other words, we already have a "super-intelligence"—it's called the internet, so just use the darn thing.
I've been working with the command line for just under two decades. A couple of years of those were spent with vim as my primary editor, but eventually I moved to Sublime and never looked back.
But I still use the command line heavily in all my work. I usually have a konsole window that I alt+tab into whenever I need to build or run tests, instead of using Sublime's "build system" support. The only time I use vim is when I need to ssh, or am using Termux on my phone.
> The proper argument here, probably, is this one: the terminal, with its way of combining small CLI tools into pipelines, covers infinitely many use cases,
Extensible GUI tools (Sublime, VSCode, etc) cover infinitely many use cases too, except they offer more reliable and reproducible runtime environments.
I think the reason these types of discussions never die is because people in general tend towards closed mindedness. It's hard to put yourself in other people's shoes, and even harder to entertain the possibility that you're wrong.
But at the end of the day this only matters for novices. After enough experience with them, no matter what you use, your productivity bottleneck isn't going to be your tools (unless its ed...).
> I think the reason these types of discussions never die is because people in general tend towards closed mindedness. It's hard to put yourself in other people's shoes, and even harder to entertain the possibility that you're wrong.
I think the real reason is that people are used to GUIs who see the "harder tools" cannot entertain the possibility that they are wrong, and see the need to constantly make these hit posts to validate themselves. I have _never_ seen a vitriolic post made by a vim/emacs/tmux/etc. user telling users to switch over - I have seen countless by the "other side". I myself switched to terminal native workflows, not because of one of these posts but despite them, seeing how people who actually used these tools came off way more positive and seemed to enjoy their work way more than I saw from people who used e.g. VS Code and endlessly complained about anything not fitting into their worldview. It's exhausting and provokes no real discussion - nobody is actually being swayed by them, and it just adds fuel to the fire, letting people with opinions swing them around
Ofc, it's less fun to accept that many of them are probably bots, but whatever.
reply