151 karma · joined February 9, 2022
It’s insanely powerful when doing by a human 100%. It’s conversely harmful when an agent manages it. There’s several papers about how LLM-managed memory is unequivocally terrible.
I am thankful for the kick in the ass for me to switch full-time into my bespoke harness utilizing open weights & GPT 5.6 and discontinue yak-shaving it with Claude Code.
> No nudity, lewdness, or sexually suggestive imagery. If it wouldn’t be appropriate for a workplace or younger audience, don’t post it here. NSFW tags are not an exception, stay classy.
Emphasis on the second sentence; where do these people work?!
the next rabbit hole starts when you try to start lifting F_2 into Z for a given <n,n,n> tensor.
I built in Human blockers into my agentic workflows with great intention, so naturally this annoyed me deeply. 14d ago, I was elated to see a random blog post that detailed the “fix” [0].
[0] https://zenn.dev/ytkdm/articles/claude-code-askuserquestion-...
I designed and stood up a sovereign inference/compute on my intranet. It uses a trust model that allows for a controller (me) to spin up untrusted inference/forge machines for Lean, Sage, or other runtimes. Untrusted sandbox workers integrate directly into my custom harness as first class “attachments.” This is the “orchestration” layer. It’s mostly on open weights, by design.
I haven’t yet started SFTing since my examples corpus isn’t quite where I’d like it.
I have solved and formalized a one non-Erdos conjecture. I have formalized several pieces of another subfield that does not exist in Mathlib yet.
As for what I am currently working on, I have an idea I want to build out about how we might think about sieving algebraic structures to generating new, insightful conjectures.
Using LLMs and distributed compute in this context is just a consequence of needing tools to help visualize or materialize things that I am otherwise bad at so I could keep doing the interesting things myself.
I still like doing maths by pen and paper, but this is fun too.
I have a couple of novel formalizations using some bolt-on programs I wrote for Claude Code, but I am mainly using it now to build my eval dataset for my custom inferencing and compute.
I won't deny the model is _pretty good_ but it is not worth all of this whiplash.
Also, what is this?
Only need ~650 tokens of system prompt for it to work. It’s pretty stellar.
- planner nodes and topo deepest for rescheduling, no inflight modifications. (repair protocol = redispatch root planner for rare cases where required; ~9% of the time for me)
- no review nodes; strongly enforced on orchestrator to always do adversarial reviews post-codegen and fix out of band
I found that putting myself in the graph is critical to ongoing fidelity, even if subpar to if I had written it all myself.
It’s shockingly effective due to rooting sub-DAGs into Planner nodes which are the only mutators of the DAG. The deepest topological leaf nodes become the blockers to the next Planner node.
The only other special node is a Human node; structurally impossible for agents to close (I rolled my own harness) and block on my attention.
You don't need to have it always on? This is a far cry from "$200/month," but I do not think it's $50k for "useful." Do you see it differently?
I made serious progress towards repairing a proof for a conjecture that was published 10 days ago but kept running into a wall with one of the Lemmas.
I threw Fable 5 Max at it with the same subagent set up and in an hour it claimed to have disproved a core theorem of the paper.
The Lean construction looks correct, but I still need to verify it rigorously. This is certainly not something Opus 4.6 Max could do and it’s likely something Opus 4.8 Max could do with more delicate orchestration and time. However, the “one-shot” Fable 5 did give me pause.
It is gratuitous to say “several,” no?
Also, for niche use-cases there are clear winners.