Very much so. It feels like it can't have been that common in the original training corpus. Probably more common now given that we are training slop generators with slop.
You are all sold this lie that "illegal immigrants take your jobs" or "bring drugs into the country", and you immediately adopt this as truth and don't even bother to fact check this because of your inherent racism.
In reality the vast amounts immigrants that are coming into US are putting 10 times back more into the economy than they are taking because they are all coming here to work. And they work at jobs that Americans don't want because they pay less. Not that there was even an unemployment crisis to begin with, so Americans had plenty of jobs.
The problem with immigration was the asylum process, where there were not enough staff to process all the requests and determine real ones from fake ones. This is why there was a border bill brought up in 2023-2024, authored by a Republican, that had bipartisan support. Trump killed that bill, saying on record that it would help his election chances. So in the end, more people would have been deported if the border bill would have passed than there are now, and there would have been way more filtering on who gets to stay and who doesnt.
All of this is true, none of this is debatable. No, your favorite right wing commentator opposing arguments are all bullshit.
And this is precisely why conservatives deserve no sympathy. Inherent racism is probably due to the shit job your parents did at raising you, which is at least excusable, but the stupidity of voting for someone who gives you the worse outcome compared to what you want, and then claiming its a better outcome, is not.
ICE is violating my fourth amendment rights as a full US citizen when they demand proof of citizenship on the sole basis of my skin tone and occupation. There is zero constitutional basis for that.
https://www.nbcnews.com/news/us-news/ice-approaching-people-...
All, no. But many, yeah. The Constitution and many of it's Amendments call out people or persons. The 14th Amendment even specifies what a citizen is, and in the next breath says persons cannot be denied due process by the States, not citizens.
No matter how many people vote for something, congress and the president do not have the right to infringe upon peoples’ fourth (searches & seizures) and 14th amendment (due process) rights. Federal agents are systematically violating those rights and not being held accountable due to a blatantly partisan supreme court. With no other alternative, it will be up to everyday citizens to stop those offenses and seek justice.
It's not just a matter of funding, but infrastructure in place (much of which constituted relationships with local communities) that Marco Rubio ordered dismantled immediately.
Think about all the things people have done in the real world the last 50 years to combat bigotry. During the civil rights movement of the 60s, black people sat at segregated lunch counters and marched peacefully in the street, and were consequently spat on and attacked by white mobs, beaten by police, sprayed with fire hoses, attacked by dogs, etc.
In the last 10 years, the modern black lives matter movement has triggered similar violent backlashes, with every public gathering drawing a militarized police response and hateful counter-protesters. On a policy level, even the most milquetoast corporate initiatives to consider applications and promotions from diverse candidates of equal merit are now being slandered and attacked. In education, acknowledgment of historical racial and gender inequality is under heavy censorship pressure.
It really does seem like the more effective we are at acting IRL, the greater the backlash is going to be.
No, it’s the most empowering thing humanity has ever constructed to wrestle the beast of IP and make it an irrelevant footnote in the human story. Deckchairs on the titanic.
If one wastes their life in court, arguing 19th century myths, that’s on the players.
IP law is not going away for “little people” like us until we collectively overturn the existing political regime which grants more rights to corporations than people.
IP being used by small firms instead of large corporations does not make it a good thing. It's the same disgusting concept to deny freedom for end users to give control to who "owns" the IP.
Yes it does, but if you think that's going to happen on its own by allowing the largest corporations to run roughshod over everyone else, you're going to be disappointed. True freedom takes struggle.
I can read and understand e.g. Python, but I have seen subtle bugs that were hard to spot in code generated by AI. At least the last time I tried coding agents (mid 2025), it was often easier to write the code myself then play "spot the bug" with whatever was generated. I don't know anything about Lean, so I was wondering if there were similar pitfalls here.
In this case the human written statement of the theorem is small. Can there be bugs? Absolutely! But it's essentially a few lines of code worth of thinking.
The lean proof checker then checks to make sure the proof actually proves the statement.
In this case an AI is generating the proof, but if it "compiles" it's correct. The only thing humans need to check is the statement to be proven.
(I don't know anything about this project but I've played around with lean and used other proof checkers more sesrisously).
This is also an issue with non-AI and non-Lean proofs. Andrew Wiles' initial Fermat's Last Theorem proof initially had an error in it. That was spotted by peer review, fixed, and an updated proof was submitted.
I don't disagree with you, but on the other hand, I feel the same way about code written by other humans, and that's not because they're necessarily worse at writing code than me, but because for code I've written myself, I've already spent time thinking about it, so I don't have to start from scratch when re-reading it. It's also not like I don't think I potentially write as many bugs as my coworkers either; it's just easier for me to catch my own up front as I'm coding than it is to catch theirs in code review. The two main differences are that I can have a more meaningful conversation with my coworkers about their approach, what bugs they might think are worth looking out for, etc. compared to an LLM (which in my experience will claim completely incorrect things about the code it wrote far more often than any engineer I've worked with even junior ones; the humans I've worked with have uniformly been able to report how confident they are in what they've produced being what they were tasked with without insane exaggerations), and that an LLM can produce a much higher volume of plausible-enough looking code in a given unit of time than most humans I've worked with. It's not obvious to me that these would be particularly severe problems in generating proofs though; unless the proof is so large that it would be infeasible to read through it in a reasonable amount of time, I would expect mathematicians to be able to make up for the lower quality conversations with the "author" by devoting more time to reading and thinking, or having someone else also read through the proof and talking through it with them. If anything, it's possible that the timeline for writing up a paper about the results might be better for some mathematicians than the equivalent amount of time most engineers have to spend reviewing code before the pressure to get it merged and move on to the next thing. (I'm aware that there is certainly pressure to get things published in academia, but I don't have firsthand experience, so I've tried to be intentional in how I've worded this to clarify that I want to avoid any assumptions about what the norms would be, but given the relatively wide range of time pressure that engineers might experience across the industry as a whole, I'd expect that at least some mathematicians might have some flexibility to spend extra time reading through an LLM-written proof, especially if it might be time they'd otherwise have to spend trying to come up with the proof themselves).
As I understand it Lean is not a general purpose programming language, it is a DSL focused on formal logic verification. Bugs in a DSL are generally easier to identify and fix.
It seems one side of this argument desperately needs AI to have failed, and the other side is just saying that it probably worked but it is not as important as presented, that it is actually just a very cool working methodology going forward.
reply