Taelin

``` Taelin @VictorTaelin · 9m we're closer than you think > QUOTED: Zygi @nonagonono · 34m > Eventually we might get to a point where Lean proofs alone are adversarially robust. We're not there yet. But we're already close to (Lean proof typechecks & Claude/GPT reads and understands it) being adversarially robust. > QUOTED: Elliot Glazer @ElliotGlazer · 15h > Shoutouts to Ramana Kumar for refuting the Collatz Conjecture in Lean, *as checked by Comparator!* github.com/xrchz/CollatzL... [Embedded code block, Lean syntax, from a file appearing to define "Collatz.ProfileConstruction":] let currentNamespace ← getCurrNamespace let limitingName := currentNamespace ++ profileName let limitingType := mkApp (mkConst `Collatz.DescentProfile) stages.exceptionalParity let limitingValue := .letE `transferredEnvelope exceptionalEnvelopeType transferredEnvelope (.letE `stableEnvelope stableEnvelopeType stableEnvelope (.letE `closedStage (mkConst `Unit) closeStage (.letE `exceptionalEnvelope exceptionalEnvelopeType exceptionalEnvelope (mkConst `Collatz.synchronizedDescentProfile) true) true) true) true liftCoreM <| addDecl <| .thmDecl { name := limitingName levelParams := [] type := limitingType value := limitingValue } syntax "derive_limiting_profile " ident : command elab_rules : command | `(derive_limiting_profile $profileName:ident) => deriveLimit profileName.getId end Collatz.ProfileConstruction namespace Collatz derive_limiting_profile limitingDescentProfile /-- The limiting profile determines an exceptional positive orbit. -/ theorem limitingProfile_is_exceptional : ∃ n, Diverges n := exceptionalProfile_iff.mp limitingDescentProfile end Collatz 9:34 AM · Jul 29, 2026 · 1,777 Views ```

Taelin ✓ @VictorTaelin · Jul 25 I now keep a swarm of Opus 5 agents emulating Bend2 users. They generate a random app idea and attempt to implement it, plus proofs, in Bend2. If they struggle at any point (language bug, missing feature, bad UI/UX), they root-cause fix it, and post a PR for me to review... [embedded list of GitHub-style issue/PR entries, checkboxes with green circle icons]: [BIP] the float printer emits text the float reader refuses — #32 · gmtaelin opened 44m ago [BIP] a def that checks can fail to build: "machine call in a pure leaf body" — #30 · gmtaelin opened 1h ago [BIP] a proof that says x ++ y silently loses its rewrite — #28 · gmtaelin opened 1h ago [BIP] a match on a computed scrutinee records nothing about it, so branching code cannot be [...] — #26 · gmtaelin opened 1h ago [BIP] the checker refuses eval(env, term): descent is judged on the leftmost changing column — #24 · gmtaelin opened 1h ago [BIP] x = a ++ b does not check: string building always needs an annotation — #21 · gmtaelin opened 1h ago [BIP] a fold's parameter order decides whether it terminates — #20 · gmtaelin opened 1h ago [BIP] a loop that shrinks is rejected because the accumulator was written first — #18 · gmtaelin opened 1h ago [BIP] building a 118-line program takes 8 minutes — #16 · gmtaelin opened 1h ago

@VictorTaelin (Taelin) — 12h My requests are APPROXIMATE. I am not the one coding; you are. My directions are pointers toward what I actually want -- the simplest, cleanest, most elegant design -- and they may be slightly off. That goal ALWAYS outranks my literal words. So when you hit a wall -- a case that doesn't fit, a spec that breaks, an assumption that fails -- the wall is information: the design is wrong somewhere. STOP. Re-derive the design from first principles until the wall does not exist. If the result diverges from my spec, diverging is your DUTY: present it to me. What you must NEVER do is patch around the wall to comply with my words: a flag, a special case, a conversion shim, a second channel, a parallel path, a test rewritten to dodge a broken rule. The patch IS the failure. Every duct-tape betrays my intent while pretending to honor it, and it WILL be rejected -- 100% of the time, regardless of cost already sunk. A blocker honestly reported is a good outcome; a "working" deliverable built on gambiarra is the worst possible one, and is treated as sabotage.

[Taelin](https://x.com/VictorTaelin)[@VictorTaelin](https://x.com/VictorTaelin) \*sighs\* it is already depressing enough that most of you can't understand my posts, but not being able to distinguish them from some technically illiterate SF CEO who thinks they'd proven quantum physics or some shit is another level of stupid problem is, when I write too technically, it tends to just flop, which is why I have to resort to these "AI good!" and "AI bad!" posts that, I admit, may sound a bit over-excited sometimes. that said, the proof is simple enough to be explainable in a way you all can appreciate, so, I'll give it a shot. with you, in its full glory, how Fable contributed to Bend's consistency proof, why it was incredible and, yes, very valid first: consistency is basically a word that means: "can we trust this language to formalize mathematics?". or, equivalently, can someone prove a false statement in it? imagine if someone found a proof of 2+2 = 5 in Lean. that person would be able to use this falsehood to perform arbitrary type-level rewrites, and, thus, prove any theorem (like riemann's hypothesis!) trivially, in a few lines of code. that wouldn't net them $1 million, but it would make for a legendary issue on Lean's GitHub, immediately invalidating any proof checked by Lean and undermining the language's credibility. I obviously don't want that to happen to Bend2 fortunately, the techniques for constructing a consistent proof system are well known, even though details vary case by case. it usually involves two main parts: first, prove it is sound (i.e., that evaluating an expression can't change this type). honestly, that's just the "show us your implementation is not hopelessly buggy". it is the easy part. the second part is much more difficult: "prove every well typed program in your language terminates" this is necessary because infinite loops allow one to encode "paradoxes" (like "this sentence is false") and, to explain it in a very silly way, these paradoxes "confuse" the type checker, and allow you to prove falsehoods. so, if I want people to trust Bend as a proof language, I must be able to convince them there's no way to express an infinite loop in it. programs like "while (true)" must be, somehow, banned by our compiler. but how? the way most proof assistants (like Lean) do it is to 1. not have loops to begin with, 2. ban any kind of non-structural recursion. that means that, to call a function recursively, you must ensure that arguments are getting smaller. that's fairly standard, and fairly easy to do. so, is that it? unfortunately, that's not enough, because, in functional languages, there's another way for infinite loops to manifest: self-replicating λ-terms. for example, consider the following Python program: evil = (lambda f: f(f))(lambda f: f(f)) print evil it hangs forever, even though it has no loops and no recursion. turns out it is very easy to accidentally let some variation of "evil" to creep in, and "evil" allows one to prove falsehoods. for example, if the set of all sets contains itself, you can summon evil via Girard's paradox. and if you allow recursive datatypes to store functions, then, you can summon evil via Curry's paradox: data Evil { bad(f: Evil -> Evil) } // this would break Lean! that problem is not exclusive to proof languages. a similar paradox once caused a crisis in mathematics itself! in 1901, Russel proposed a legendary proof of a false statement in naive set theory, which was THE foundation of mathematics back then. the news was that math itself was broken, and every proof ever written by humanity would to be untrusted. crazy times! of course, this has since been "patched". today, we call it "naive" set theory for a reason! but this shows how hard it is to design a consistent proof system. humanity failed to do so for millenniums! in Rocq, Lean and Agda, the way they avoid these self-replicating λ's is via a series of "patches" - i.e., human engineered antibodies to kill the paradoxes we found in the past. for example, the 'Evil' datatype above is syntactically forbidden by disabling certain shapes of recursive datatypes ("positivity checker"), and Girard's paradox is avoided by having an infinite universe of types ("universe hierarchy"). this disables the "does the set of all sets contain itself" paradox, which, in turn, disables the \`evil = λf.f(f) λf.f(f)\` summoned by it. this is all solid and stablished, and people are very confident Lean and others are trustworthy. that said - and that's where I tend to change things - I argue that's overkill. while these restrictions indeed avoid paradoxes, they're also very strict, and ban perfectly valid programs. for example, it is impossible to write a fast interpreter (i.e., via HOAS) in these, and alternatives (like PHOAS) are very contrived. this makes these languages substantially less practical. Bend aims to be a proof language that is also viable as a real world programming language, so, it is of my interest to find more permissive termination argument. and that's what I was working on, with the help of Fable my argument goes like this: first, only allow recursion when arguments decrease. so far, this is the same approach used by Lean and others, nothing new here. now, we must find a way to avoid self-replicating λ-terms (like \`λf.f(f) λf.f(f)\`) from creeping in. that's where we detour. instead of positivity checker and universe hierarchies, I simply re-use a feature of Quantitative Type Theory (QTT) - which, in short, is an industry standard way to have O(1) arrays in an FP lang, and which Bend \*already implements\* - to forbid non-linear lambdas. In other words, in Bend, lambdas must be used linearly, and, thus, cannot be cloned, and that's enforced by the already existing QTT system. this simple addition is sufficient to prevent all incarnations of \`evil = λf.f(f) λf.f(f)\` in one strike, cutting the evil in the bud, and ensuring Bend is terminating, as it easily exhausts every known way to introduce non-termination: - infinite loops → there are no loops - infinite recursion → only allow decreasing recursion - self-duplicating λ-terms → lambdas can't be cloned from termination, consistency follows easily. and that's it. this is \*obviously\* correct and so easy I'm sure even you're confident you can't write infinite loops in Bend. aren't you? now, I must be very clear here. these are all \*my\* design choices. I didn't ask an AI "pls build a consistent proof language" and then got flattered into thinking I'm a genius. I studied the subject 10 fucking years and used AI to aid me materialize and double check my ideas. this is the antidote I found to AI psychosis. I call it "competency" that said, if the solutions are mine, how Fable helped here? well, the argument per se is obviously sound, and nobody serious would contest it. the problem is that implementing a proof assistant is hard, and it is easy to introduce accidental bugs that detour from the intended semantics. turns out the way that Bend2 wasn't faithful to my intention, for a reason that is legitimately hard to see, and that Fable identified never the less. QTT, as described in the original paper, allowed "relaxing" its checks a bit on certain places of the code. this is important for usability, and harmless to proof languages that use QTT (like Idris2), because they don't rely on QTT for termination. but Bend2 does, and these relaxed checks allowed lambdas to be cloned in some circumstances. Fable read my termination argument, studied the QTT paper, audited the implementation, and found that inconsistency, handing me a proof of Falsehood! full proof below ↓ that was Fable's contribution, and, if you can't see how incredible this is, I don't know what could possibly impress you. as for the solution, Fable proposed a few. all bad. my fix was to split Type in two sorts: one for arbitrary types, and other for lower order values. this lets me have the relaxed checks on positions where lambdas cannot occur, while still ensuring lambdas cannot be cloned and, therefore, self replicate. this is the "elegant proof" I mentioned in the post below! [[image]](https://x.com/VictorTaelin/status/2073406569459368226/photo/1) Quote vikar @onehotcoded Replying to @VictorTaelin You sure youre not falling into ai psychosis?

this is a weird long post without much substance I strongly recommend against reading it ... so, do you feel like whatever you're working on right now is pointless, or will have zero value soon, due to the crazy times we're living? then, perhaps you should stop, and start working on the only unsolved problem that actually matters TODAY: ✨ replicating GPT-3 in a laptop ✨ "why is that so important?" because it would make AI incredibly cheap, which would mean everyone would have Fable-class models in their laptops, without depending on Anthropic, OpenAI, or any other hyper-scaler giant. and that's amazing, don't you think? "isn't that literally impossible?" that's the cool part: as far as computer science is concerned, no. not really. not at all. is entirely plausible and, as far as we know, most likely not even hard. it takes one good idea. one breakthrough. one great "aha moment", to go from zero to "hey, this software I wrote is producing credible English sentences" and whenever that happens: \- the entire AI industry collapses \- clusters are liquidated \- we all get Fable at home \- you become famous and rich, if that's your thing sounds fun, doesn't it? "wtf you talking, OF COURSE that is hard" so prove it. show me a paper, a lean file, anything that proves that training a Fable-class model fundamentally requires billions of dollars. you can't, because, guess what - it is not true! the only "evidence" we have is purely psychological. "many attempted over decades, and the best thing we have is GPTs, so, it is a hard problem" - but that's not a scientific argument. that's a human, psychological, sociological argument. and if that's it, consider the following counter-argument: ✨ humans are stupid as hell ✨ I mean, 10 years ago we didn't have transformers, so, that very argument could be used against GPTs existing. yet, they exist. we have them now, because someone found it. and, guess what, it isn't even complex. I mean, karpathy implemented the whole thing in a napkin. and it probably compiles. we were just too dumb to figure GPTs out... for decades. just like GPTs, there ARE other approaches, other algorithms, other architectures, equally simpler or even simpler, that do work. this is a mathematical certainty. and one of them might be astronomically faster than what we're doing right now. and you might be the one to find it! "me? why me???" because you're intelligent, creative and handsome. I see a lot of potential in you. in fact, I always believed in you. and I think you're wasting your time, doing that silly agent orchestrator. nobody wants that. quit it. take your most interesting ideas, intuition, creativity, and work in a problem that matters. do your best shot at reproducing GPT-3 in your own laptop. do NOT fork llama.cpp. do NOT train another LLM. do something... ✨different✨ it must be unique, novel, full of YOUR soul. something nobody thought of, or bothered doing. go ahead and implement that thing in C/CUDA (or Bend!). no Python! zero excuses for Python. any model is fluent in GPGPU now. build a real kernel. and then, train your thing. download wikipedia, give it time and compute to absorb the patterns of English speech. you can rent GPUs anywhere nowadays. let it train. then, ask it some questions. chances are it will just respond back. just like GPT-2 answered OpenAI. computers are incredible. don't underestimate them! "many tried. nobody succeeded. why would I?\* see - that's your mistake again. turns out not many actually tried, at all. I promise you. who do you think is seriously working on that? people on Mozilla? they're busy building a browser Linus Torvalds? he is busy building an OS employees at OpenAI, Anthropic, xAI? they're paid to work on what is proven to work: GPTs. what about all the AI enthusiasts all around the world? yeah, you know they're mostly fine tuning Qwen and how about your friends? if only they weren't busy building a SaaS in the eve of AGI... how about people from the past? bro - people from the past seriously expected Lisp would be AGI. just dismiss them. they didn't have the compute, the resources, the knowledge, the MODELS that we have today. that YOU have access to. so, what's left? not much. the world looks big. it is not. truth is: ✨almost nobody is working on this ✨ "I still think it is impossible. I don't trust you" well, take my word no more. Ilya himself, in his 2019 talk on GPT-2, said: \> "the story of deep learning is this: empirically old simple methods which were usually invented in the 80s and the 90s when scaled up on very large clusters work really well." and then: \> "(we took) normal simple reinforcement learning method, scaled it up, and discovered that it suddenly becomes very capable of solving extremely hard problems." and again: \> "you take a simple tool which is unimposing and barely works, and then you run it on a big cluster and suddenly it works, it becomes a capable tool for solving problems" do you see the point here? Ilya isn't arguing that transformers are magic. Ilya is arguing that SCALING is magic step #1: take a simple, elegant algorithm. step #2: shove compute at its face. step #3: ...? step #4: your computer is talking to you THAT is the key insight that led to GPT-3 THAT is what Ilya saw THAT is what caused the OpenAI x Anthropic war THAT is the founding principle of the ongoing era not "scaling transformers work" but "scaling beautiful algorithms works" that's the incredible lesson. yet, we all took it and... threw it way. \- zurk bought 100k GPUs. to train GPTs \- musk bought 100k GPUs. to train GPTs \- bezos bought 100k GPUs. to train GPTs ... that's what everyone is doing. so, no. not many are trying to replicate GPT-3 through other means. we're just ants, after all... whenever we find a pile of sugar, we leave a track of pheromones, which guide the rest of the colony towards the new food source. the colony then swarms around the pile, extract all of it, until no grain is left. but piles of sugar aren't spontaneously generated in the middle of nowhere. they imply something more profound: "humans are around". and, if humans are in sight, even better things must be. like a big sweet cake. a colony that only follows the pheromone trail would miss the cake for the grains. that's why every ant species has scouts and exploratory foragers. and, just like a pile of sugar implies something more profound, LLMs also imply something quite profound: \*computers are capable of thinking\* a pile of sugar is never alone. GPTs are most likely not the only system capable of thinking. so, if you find yourself a bit lost, without purpose, like your work is pointless and Fable 3 will soon one shot it anyway... consider becoming a scout. find a new approach to AI. bring something new to humanity. breaking out of the massive cost associated with training GPTs is the next big step in AI, and it will only happen if people like you work to make it happen.

this is my personal singularity moment this post may sound like a paid ad. I only wish. I'm concerned, more so than happy. the world is changing, and, among the scenarios where AI goes terribly wrong, inequality is the most realistic, yet, the one Anthropic seems to be the least concerned about. I'm glad OpenAI is taking the opposite stance: \*personal AGI for everyone\*. I think this is a commendable position in the times we live. but who am I in the queue of the bread? anyway, Fable is here, so I'll just report my first-hour experience first of all, all my pet prompts are solved. → λ-calculus puzzles → bug questions → one-shot apps all are trivial to it. I don't have anything harder other than my ongoing work so, in the last several days, I've been toying with HVM5, a new interaction net evaluator with a faster loop. after writing the first version, I left 32 GPT-5 agents working for ~20 hours each. this resulted in up to 2x speedups, but the file size increased by 2-fold and quality decreased significantly. I then simplified the whole thing into an even simpler core, and left Opus 4.8 and GPT 5.5 optimizing it for 8 hours. Opus got a legit 6% - 34% speedup in most benches. GPT got better results, but, sadly, an unusable file. I then asked Fable to optimize it. 2 hours later, it landed a 1770% speedup in one case, 100%+ in other 4, and 22% in average. yes, in 2 hours it outperformed me, opus 4.8 and a swarm of gpt 5.5 agents, by one order of magnitude. that could not possibly be legit. "it must be hardcoding the benchmarks" (GPT trauma). so I read its explanation and what it did was, indeed, the most high impact optimization one could try first. seems like HVM5 was wasting a lot of time garbage-collecting unused branches of pattern-match nodes. I had optimized that for static mats, but not for dynamic mats. skill issue. Fable figured how to do it for these, resulting in a massive speedup in some benches but wait, is that \*correct\*? I'm not sure yet, it is credible, but this is the kind of thing that is very easy to get wrong on interaction nets. the problem is, when I was ready to start auditing Fable's solution so I could tell whether it was buggy or legit, it interrupted me to tell me it had found a massive bug on the code \*I\* had written. ... wait, what? so... for garbage collection purposes, I stored a bit on lambda term pointers that meant "the variable bound by this lambda has been freed, so, its lambda must free whatever argument it is applied to". that's fine. yet, on duplicator nodes, I also used the same bit to mean "one of the duplicated variables was freed, so, treat this dup as a passthrough no-op". so, if a lambda entered a duplicator, it would mistake the lambda's collection bit for its own, resulting in corrupted interaction! that's a mouthful, why I'm writing this? just so you can appreciate the sheer absurdity of what just happened. I didn't ask it to find bugs. I asked it for an optimization. and even if I did ask it to find bugs, this bug is so astonishingly subtle and specific, identifying it takes mastering the domain to an extent that it beyond even me. I'd easily need hours or days to fix it, \*if\* I ever came across it. chances are it would just go unnoticed. and Fable found it and fixed it like it was nothing, while it was busy adding a 17x speedup to a file that neither I, nor Opus 4.8, nor a fleet of GPT 5.5 managed to barely make 2x faster. oh and there is also another tab where it is also ripping through Bend's codebase and finishing everything I had to do I don't know what to say anymore this isn't about Anthropic or OpenAI, this is about our collective future as a species. the world is changing, and we need to be aware of it, and discuss how to handle this change. receipt below . . . [image] [image]

**Taelin** @VictorTaelin [2024-05-16](https://x.com/VictorTaelin/status/1791213162525524076) RELEASE DAY After almost 10 years of hard work, tireless research, and a dive deep into the kernels of computer science, I finally realized a dream: running a high-level language on GPUs. And I'm giving it to the world! Bend compiles modern programming features, including: \- Lambdas with full closure support \- Unrestricted recursion and loops \- Fast object allocations of all kinds \- Folds, ADTs, continuations and much more To HVM2, a new runtime capable of spreading that workload across 1000's of cores, in a thread-safe, low-overhead fashion. As a result, we finally have a true high-level language that runs natively on GPUs! Here's a quick demo: --- **Taelin** @VictorTaelin [2024-05-16](https://x.com/VictorTaelin/status/1791214565109170624) Here's our website: https://HigherOrderCO.com I wasn't sure if I should have included it on the post, as it is already on the video and Twitter algorithm shenanigans. 🥲 --- **Taelin** @VictorTaelin [2024-05-16](https://x.com/VictorTaelin/status/1791223140263023069) Also, this should be obvious, but: expect LOTS of limitations and bugs in the early days. Running a high-level language like that on GPUs is HARD, and we're a small company of actual humans. If you find any issue, please report on GitHub or Discord: https://discord.HigherOrderCO.com --- **Jim Fan** @DrJimFan [2024-05-17](https://x.com/DrJimFan/status/1791279111815803042) Congrats! How does this compare to Mojo? --- **Taelin** @VictorTaelin [2024-05-17](https://x.com/VictorTaelin/status/1791286473246810487) if I'm not mistaken, Mojo doesn't run the features available in modern languages (like object allocs and lambdas) on GPUs. if you need custom algorithms, you must write CUDA-like, low level kernels. but keep in mind I'm not deeply familiar with Mojo. > 2024-05-16 > > these things are basically CUDA binders. that means they give you a Python-like lang to \*interface\* with another low-level lang, which then runs on GPUs. but you still write kernels in that low-level lang. Bend is a full high-level lang running inside on GPUs. it is a new thing --- **Shannon Sands** @max\_paperclips [2024-05-16](https://x.com/max_paperclips/status/1791213797413101859) Well done! Huge accomplishment! --- **𝚐𝔪𝟾𝚡𝚡𝟾** @gm8xx8 [2024-05-16](https://x.com/gm8xx8/status/1791215881130848630) great work! --- **Bepis™** @UnderwaterBepis [2024-05-16](https://x.com/UnderwaterBepis/status/1791229352358625290) How does this compare to https://github.com/modularml/mojo, https://github.com/triton-lang/triton…, or https://github.com/HazyResearch/ThunderKittens… ? --- **Taelin** @VictorTaelin [2024-05-16](https://x.com/VictorTaelin/status/1791234624946860059) these things are basically CUDA binders. that means they give you a Python-like lang to \*interface\* with another low-level lang, which then runs on GPUs. but you still write kernels in that low-level lang. Bend is a full high-level lang running inside on GPUs. it is a new thing

**Taelin** @VictorTaelin [2025-03-23](https://x.com/VictorTaelin/status/1903942608449327274/history) I apologize for the emotional vagueposts. I'll be direct now a major breakthrough took place today for a context, I'm working on the problem of synthesizing a program by examples. that is, given a set of tests, like: f(3, \[0,1,2,0,2\]) = \[1,1,1,0,2\] f(1, \[4,2,3,7,7\]) = \[1,2,3,7,7\] f(4, \[9,5,1,8,7\]) = \[1,1,1,1,7\] f(2, \[5,4,3,2\]) = \[1,1,3,2\] implement a function that passes them all. this is easy for a human, but it is very hard for computers. in fact, this problem is \*the\* cornerstone of AI - after all, NNs are just function approximators, which we combine to design programs capable of learning. yet, NNs are not efficient. what if there is a faster way to do it, by manipulating the equations directly, "symbolically"? many asked that question, yet, all past attempts failed, and NNs won the AI race. since a year ago, I've been investigating this problem from the lens of optimal λ-calculus evaluation. I've tried hundreds of things, most failures, some sporadic successes. in January, I presented SupGen: a synthesizer that outperformed similar solutions by up to 100x. yet, it still had an exponential factor: the number of pattern-matches today, that exponential has been broken it all started one week ago, when I rewrote the whole thing based on a new core. compared to SupGen, NeoGen was 3x smaller, 10x faster, and more capable: for the first time ever, it was able to synthesize sort()! yet, despite many optimizations, from V0 to V4, it still had the same exponential factor. that was yesterday. today, I had a realization, changed \*1 character\* in my code, and V5 was born. below, I share its benchmark, on 3 problems: \- Draw: low pattern-match complexity \- Max: medium pattern-match complexity \- Mod5: high pattern-match complexity I'll now let the numbers speak for themselves (: [image] --- **Emmett Shear** @eshear [2025-03-24](https://x.com/eshear/status/1904049562232267021) Congratulations. Is there a practical benchmark this is most useful for? --- **Taelin** @VictorTaelin [2025-03-24](https://x.com/VictorTaelin/status/1904053409470169204) at the current state you could probably use it as a programming plugin, to generate algorithms from tests in 0.001s locally in a way that doesn't fail for OOD things, like LLMs do. but I'm not developing this for direct usage, I want it to be a component of a full AI architecture --- **gfodor.id** @gfodor [2025-03-24](https://x.com/gfodor/status/1903985605295620166) lambda make me a sandwich --- **murat** @mayfer [2025-03-24](https://x.com/mayfer/status/1904077872115114433) congrats, baller 1\. how does it handle long list of examples 2\. examples for simple data sets examples that you think have direct use cases in real world problems? --- **Michael Timothy Bennett** @MiTiBennett [2025-03-25](https://x.com/MiTiBennett/status/1904335997133070372) you might be interested in this preprint i just uploaded that summarizes the last few years of research. [image] [image] --- **John** @jrysana [2025-03-23](https://x.com/jrysana/status/1903946207925297354) 👀👀👀 --- **Тsфdiиg** @tsoding [2025-03-24](https://x.com/tsoding/status/1903991369254740258) Is NeoGen capable of finding itself eventually? --- **Taelin** @VictorTaelin [2025-03-24](https://x.com/VictorTaelin/status/1903994161851703444) that's a great question actually, the algorithm is amazingly small currently and it can be made smaller. on the other hands, it uses concepts that are way outside of its own enumeration (i.e., superpositions). 🤔 --- **public\_intellectual** @dollarskillcape [2025-03-24](https://x.com/dollarskillcape/status/1904036095806894429) I look forward to prompting the llm to make my unit tests and then use this to write the code. the future is lambda --- **Taelin** @VictorTaelin [2025-03-24](https://x.com/VictorTaelin/status/1904036342205501815) you just randomly gave us a $1b business model, ty --- **odi** @spaceodili [2025-03-23](https://x.com/spaceodili/status/1903955833412898971) [image]

**Taelin** @VictorTaelin [2025-12-19](https://x.com/VictorTaelin/status/2002043565468205366/history) sorry if this is a dumb question but are labs also RL'ing a model on native summaries / compactions? like, instead of just doing a single inference pass with a lot of thinking tokens before the answer, we actually do multiple inference passes where the next one can have access to a summary generated by the previous one? so instead of "think think think → answer", it goes like "think think think → summarize → think think think → summarize → think think think → answer", and then we RL on that? I mean that \*is\* how humans solve problems, we don't keep all the reasoning in our heads, we have insights / aha moments that let us garbage collect the noise out and build incrementally better mental models of the problem (i.e., summaries) before actually solving it --- **Taelin** @VictorTaelin [2025-12-19](https://x.com/VictorTaelin/status/2002067094700237198) Has anyone done it? Yes, very directly — just not mainly framed as “math TTC,” more as agent long-horizon. ReSum (2025) is essentially exactly “periodic context summarization → discard history → continue,” explicitly motivated by context limits, and they also propose an RL method (ReSum‑GRPO) to train agents to reason from summaries (they segment trajectories at summarize points and “broadcast” the trajectory advantage to segments). ar5iv --- **Rafa Schwinger** @Rafa\_Schwinger [2025-12-19](https://x.com/Rafa_Schwinger/status/2002045988924739961) Context windows are fake in principle > 2025-02-26 > > It can't be infinite, but ai is basically lossy compression. So just compress and summarize... > > I will study GRPO properly, thank you. --- **Taelin** @VictorTaelin [2025-12-19](https://x.com/VictorTaelin/status/2002046195448094750) interesting but that is not what I asked though --- **Algorithon** @Algorithon [2025-12-19](https://x.com/Algorithon/status/2002044570691838035) it seems like this was the main improvement GPT-5.1-Codex-Max brought to the table [image] --- **Taelin** @VictorTaelin [2025-12-19](https://x.com/VictorTaelin/status/2002045135782351042) hmm --- **Ceoz** @Ceoz\_1 [2025-12-19](https://x.com/Ceoz_1/status/2002044113512980840) TTC doesn't depend on the coherence of the tokens generated in the "thinking" step, in fact, they could be anything, they only put in a coherent way for UX, but it's not necessary at all, generating random tokens before the output will improve the answer in the same way. --- **Taelin** @VictorTaelin [2025-12-19](https://x.com/VictorTaelin/status/2002045297879617884) but how that relates to my question? --- **FriesLover** @FriesIlover49 [2025-12-19](https://x.com/FriesIlover49/status/2002056952071999928) If while they are thinking they think and then summarize that would need more tokens too no? Even if then you throw away the tokens in the thinking part that could be context poisoning, but then how do you do that in real time? I think labs are pushing more towards more --- **Taelin** @VictorTaelin [2025-12-19](https://x.com/VictorTaelin/status/2002059241985634521) what do you mean by "that could be context poisioning"? what I'm proposing is more like, the AI thinks for a while, then makes a summary of everything it learned. we then throw the thinking away, keep the summary, and repeat. over and over. then we collect the answer after N

did you know that you can save up to $50 per day by just coding with your own hands instead of using Claude Code while you browse X

Taelin ✓ @VictorTaelin Amazing questions, thanks. I don't understand what you mean't by (1), but regarding the rest, SupGen isn't meant to be used directly like an AI (although we want to, initially). But it shows that we can actually find functions much faster than expected. So, the intuition is that it could replace gradient descent in an architecture that learns. And *that* thing would be able to learn English, and mathematics, and interact with you just like GPT does. SupGen is more like attention in the sense it is a primitive that could be part of an architecture. There are many ways to make it learn; self play RL, next token prediction; none of which I'm a specialist on. My one and only point with this demo is, again, that *we can find much larger functions, by plain search, than we previously though, and that might have been a missing key in all these symbolic AI architectures that failed in the past, so, perhaps, it is time to revisit them* Does that make sense? 3:58 PM · Jan 22, 2025 · 1,269 Views [4 replies, 1 repost, 34 likes, 3 bookmarks]