A harness [1] was developed by Terrence Tao and some collaborators to prove mathematical results. It has since then been used by others with positive effect. Can someone critique the structure of this harness? I don't know anything about this stuff. [1] https://github.com/1stproof/batch-2/tree/main/batch-2-submis...
it's not actually proving it though? It's more like stringing it together. A person or LEAN has to actually provde something. I've yet to see anything other than AI-slop produces simulcra of proofs. If it were proving something it'd be validates AI proof.
Building an Advanced Agentic Harness
31–40 of 47 posts
Re: Building an Advanced Agentic Harness
#32Re: Building an Advanced Agentic Harness
#33Earlier quoted context omitted.
it's not actually proving it though? It's more like stringing it together. A person or LEAN has to actually provde something. I've yet to see anything other than AI-slop produces simulcra of proofs. If it were proving something it'd be validates AI proof.
I don't you what you mean. People have used the above harness (or similar) to prove significant results. See this recent paper [1], which claims > The human authors take full responsibility for the claims and proofs contained in this paper, and have carefully refined and verified them. The construction and main ideas of the proof were generated entirely by Codex using GPT 5.6 Sol Ultra, using harness ideas generated…
A model is non-deterministic. People prove things, LLM string together a bunch of words and do symbol shunting.
Ensure you understand what symbol shunting is before you make claims. https://ell.stackexchange.com/questions/76400/what-does-one-...
Real break throughs come from integral mathematics and not just a few reorderings. I've no doubt these are talented people recognizing output as useful; however, every time I see these links presented it's never from the "Prominent mathematician verifies AI proof"
Don't put the cart before the horse if you want people to think LLMs are cracking math problems in real terms.
Re: Building an Advanced Agentic Harness
#34Earlier quoted context omitted.
it's not actually proving it though? It's more like stringing it together. A person or LEAN has to actually provde something. I've yet to see anything other than AI-slop produces simulcra of proofs. If it were proving something it'd be validates AI proof.
Stringing what together? A sequence of logical implications? The word for that is "proof".
A collection of logical implications proof.
Re: Building an Advanced Agentic Harness
#35But pulling orchestration off is very very tricky.
Even if it is just a small, simple orchestrator.
Ideas like planner, memory, log, subagents, graphs (each on their own) sound great and very promising.
So promising that one would think they must work, how could they not?
I've been there as well!
The challenge is that all these parts of the orchestrator are intertwined with each other
and they are all causing overhead in the main context window in some form or at least overall complexity that is difficult to grasp and predict/engineer for
(even though the idea is to help exactly with the fact that the context window is limited)
To save context window there is also more communication that has 'stille post' ('chinese whispers') like dynamics
Turns out it is very difficult to find out the right context to bubble up and down.
It's very similar to human org communication challenges (think large org stucture vs small teams vs one person that can keep it all in their head)
Yeah, what do you do if one person can't keep it all in their head?
But how great is it when it's possible?
Companies must have figured out how that works right? Maybe we can adopt and implement these ideas?
And yet … easy it is not, especially when you're not dealing with run-of-the-mill well-defined tasks.
But more like with open-ended software development?
I'm not saying it's not possible or that it should not be tried.
On the contrary, I think this is worth pursuing and a bit like the search for the holy grail.
But I also think the other direction of the search space is under-explored.
The holy grail is glamorous.
With 'smol' I'm spelunking on this other extreme (non-orchestration?)
(welcome, join us, we have cookies, and context windows with a lot of room for work items!)
smol is a minimalist agent harness that protects the context window
- no system prompt
- no tool spamming (just 1 tool: sh)
- no agents.md
- no mcp
- no planning, todos, graphs, beads, …
and figuring out how that looks like and performsit is a worthwhile thread to pull I think
at least from the dozens of benches I'm looking at I see that less stuff in the context window does help a lot
- cheaper per task
- finishing faster
- better tool composition (sh and pipes are great!)
but also for more complicated longer-term tasks the model gets less confused when the context window is not getting spammedthe context window is precious
Re: Building an Advanced Agentic Harness
#36Any benchmarks showing if this actually improves problem solving? Or reduces errors? The idea is cool, but from own experience in harness engineering, lots of cool sounding ideas can have a negative impact on performance due to emergent and confounding effects. So I'm a bit skeptical!
The TUI and Session manager are straightforward enough. PI is serial by default but can become more DAG-like, where Codex is designed specifically for DAG and this is going more the Codex direction. I'm much more interested in the memory model and why. As far as I can tell, it's "a vector Db" and not much more is said. Nothing about working memory or procedural memory (there are lots of ways to classify it, https://w…
"Answer": a word soup that in no way, shape, or form addresses the question, but does sound jargony and vague enough to be an LLM.
Re: Building an Advanced Agentic Harness
#37I love reading about orchestration concepts. But pulling orchestration off is very very tricky. Even if it is just a small, simple orchestrator. Ideas like planner, memory, log, subagents, graphs (each on their own) sound great and very promising. So promising that one would think they must work, how could they not? I've been there as well! The challenge is that all these parts of the orchestrator are intertwined wit…
Re: Building an Advanced Agentic Harness
#38I love reading about orchestration concepts. But pulling orchestration off is very very tricky. Even if it is just a small, simple orchestrator. Ideas like planner, memory, log, subagents, graphs (each on their own) sound great and very promising. So promising that one would think they must work, how could they not? I've been there as well! The challenge is that all these parts of the orchestrator are intertwined wit…
I read some of your twits but could find the source for that, do you publish it?
Re: Building an Advanced Agentic Harness
#39So maybe that's a big chunk of what you need for an 'AI Company': an agent that manages the goals and hierarchies. Although of course the DAG and agent hierarchy is not quite the same thing. But maybe the workflows and subworkflows are what matter.