It is not like their knowledge and experience gets literally purged.

> 7. You must not share projects that mostly consist of code written by "generative AI"-tools (including services such as Claude, OpenAI Codex). Such projects having an unclear copyright status (see requirements § 2 (1) 1 and § 2 (1) 3) and furthermore have little safeguards to ensure that they do not include harmful code (c.f. § 2 (1) 5).

The industry and users moves on from single chat-based to more and more "agentic" workflows that may generate longer workloads with multiple simultaneous agents (separate agents - separate contexts - separate KV caches).

My estimation is based on, say, running a Kimi3 on a 24 B200 GPUs - it is very easy to lose money when selling tokens at "market" prices.

* Check if 1M context is disabled via environment variable.

* Used by C4E admins to disable 1M context for HIPAA compliance.

*/ export function is1mContextDisabled(): boolean {

  return 

}

Interesting, how is that relevant to HIPAA compliance?

Now that I think about it, most of my advice starts something like "Here's what you're gonna do..."

Wait, that itself sounds like a problem, but how do I fix it...

I just glanced at the IR which was different for some attributes (nounwind vs mustprogress norecurse), but the resulting assembly is 100% identical for every optimization level.

Quoting one of the recent papers (2020):

> With current technology, it would take many person-decades to formalise Scholze’s results. Indeed, even stating Scholze’s theorems would be an achievement. Before that, one has of course to formalise the definition of a perfectoid space, and this is what we have done, using the Lean theorem prover.

Feynman: "What I cannot build. I do not understand"

Einstein: "If you can't explain it to a six year old, you don't understand it yourself"

Of course none of this changes anything around the machine generated proofs. The point of the proof is to communicate ideas; formalization and verification is simply a certificate showing that those ideas are worth checking out.

Usually the point of the proof is not to figure out whether a particular statement is true (which may be of little interest by itself, see Collatz conjecture), but to develop some good ideas _while_ proving that statement. So there's not much value in verified 1mil lines of Lean by itself. You'd want to study the (Lean) proof hoping to find some kind of new math invented in it or a particular trick worth noticing.

LLM may first develop a proof in natural language, then prove its correctness while autoformalizing it in Lean. Maybe it will be worth something in that case.

> It is rather well-known, through Peano's own acknowledgement, that Peano […] made extensive use of Grassmann's work in his development of the axioms. It is not so well-known that Grassmann had essentially the characterization of the set of all integers, now customary in texts of modern algebra, that it forms an ordered integral domain in which each set of positive elements has a least member. […] [Grassmann's book] was probably the first serious and rather successful attempt to put numbers on a more or less axiomatic basis.

I've come across TLA+ multiple times, but it seems it was more targeted towards distributed systems (Lamport being the creator, that makes sense). Is it correct, that it would be useless in other domains?

I suppose that one of the pros of using tree-sitter is its portability? For example, I could define my grammar to both parse my code and to do proper syntax highlighting in the browser with the same library and same grammar? Is that correct? Also it is used in neovim extensively to define syntax for a languages? Otherwise it would have taken to slightly modify the grammar.

I wonder, what is the actual blocker right now? I'd assume that LLMs are still not very good with specifications and verifcation languages? Anyone tried Datalog, TLA+, etc. with LLMs? I suppose that Gemini was specifically trained on Lean. Or at least some IMO-finetuned fork of it. Anyhow, there's probably a large Lean dataset collected somewhere in Deepmind servers, but that's not certification applicable necessarily, I think?

> AI also creates a need to formally verify more software: rather than having humans review AI-generated code, I’d much rather have the AI prove to me that the code it has generated is correct.

At RL stage LLMs could game the training*, proving easier invariants then actually expected (the proof is correct and possibly short - means positive reward). It would take additional care it to set it up right.

* I mean, if you set it to generate a code AND a proof to it.