> The workflow I had in mind was deliberately cautious

> The code was not the difficult part.

> These requirements are not a one-time form to complete and forget. They create an ongoing responsibility around the account, the documented process, community feedback, failures, and potential reversions.

Just a few examples. And yes, Pangram 4 also flags it as 100% LLM written. I don't mind being downvoted or flagged, but I think more people should be aware of the LLM style, even if they're ok with it being used without any disclaimer. It's honestly sad that nowadays people on HN cannot recognize this style.

> The gap has two independent consequences, each sufficient to invalidate the claimed disproof. The first is structural.

Then the classic coding agents negation of earlier evidence, instaed of just updating to use new references, they mention that they changed old to new:

> The publicly released monolithic file ConnesRigidity.lean (37,000+ lines) does not use the names CocycleExtension, ZeroCocycle, or TwistedCocycle that appeared in the earlier modular source files (CocycleExtension.lean, ICC.lean, CrossedClosure.lean). However, the identical mathematical construction is present under different names. The following table gives the correspondence, with line numbers in the published file.

> This is the same zero-cocycle / twisted-cocycle structure identified in the earlier modular source files, confirming that the structural analysis of this note applies to the published code

And some other Claud-y stuff:

> Why both paths are closed. A successful defence would have to close both paths simultaneously

> This case illustrates a failure mode that is becoming increasingly well documented in the literature on AI-assisted formal mathematics: the gap between what a formal proof verifies and what it means. The Lean kernel certifies that a proof term inhabits a given type; it does not certify that the type faithfully encodes the intended mathematical claim. As Tao has emphasised

And afterwards I cross-verified with Pangram 4 which I trust, it marked the preamble/starting stuff as 100% AI-generated.

Comments URL: https://news.ycombinator.com/item?id=49025154

Points: 2

# Comments: 0

UPD: The edit got reverted and there's this on the talk page now: https://en.wikipedia.org/wiki/Talk:Jacobian_conjecture#c-DaR...

UPD2: There are edit wars happening now: https://en.wikipedia.org/w/index.php?title=Jacobian_conjectu... https://en.wikipedia.org/wiki/Talk:Jacobian_conjecture#c-Sea...

It's extremely clear you're not writing those yourself, which makes the whole thing very disingenuous if you can't engage with others in your own language.

Maybe you should start by not writing your HN posts with an LLM..

1. Your window ends (usage reset) in 3 days

2. They reset usage for everyone

3. Your usage goes back to 100% and your current window ends in 7 days now.

It's very interesting that for Anthropic the $100 and $200 plans only differ 2x in weekly limits, the 5 hour limit differences are more severe. But for OpenAI, Pro 20x is, well, 4x of Pro 5x for only 2x cost. So, for example, 100% of weekly usage for Codex on a Plus ($20) account is just 5% of weekly usage for Codex on Pro 20x.

And you can calculate how much extra usage you can get from resets, and especially banked resets by purposefully using the whole quota and using your banked reset - they expire 30 days after they're given out, so if you don't use one, it just disappears.