fractorial

To be clear, I am deep into auto-research, but hooking up slop to slop is just unlikely to produce anything valuable.

Value is in how maths is communicated: The process, frustrations, triumphs, etc.

We have to able to take generated formalizations from “it compiles” to “it is correct” before crystallizing them.

Irrespective of opinions about a project or its authors, disclosing a potential security issue in a public forum is markedly not responsible disclosure.

This is, plainly stated, awesome.

I would love for someone to give me a coherent argument as to how this isn’t tone-deaf, vacuous garbage.

I can’t say much for a Chief Evangelist, but the Product Manager certainly has quite the C.V.

Actual link to source material: https://zenodo.org/records/21871667

It appears that there is no machine-checked proof or corroboration of this claim; I would be dubious in calling this “solved.”

Fascinating approach; however, a nightmare to scroll on mobile.

For context, I've rolled my own research harness in Go; I've been trying very hard to keep the non-test LOC around ~30k lines. To me, I consider this large, but necessary, especially after meticulously crafting red diffs while adding features.

I do use it to work on itself. I agree smaller is likely easier to work with; however, that's still, at least partly, disjoint from binary size.

I’m not quite sure why the harness itself needs to be small. Isn’t the system prompt and management of system prompt the bit you want lightweight?

I similarly find it interesting; I do not understand why it is not the default to just generate the thing as a draft, research anything you aren’t clear on, and re-write it in your own voice.

Cosmically apt username given the substance of this comment.

It would appear that rolling my own Anthropic-free harness / serving stack with a closed-weight carve out for Codex models is an absolute win.

> Do anti-LLM types expect to be vindicated in an orgy of copyright lawsuits that resets the industry back to 2022? What do people pushing expect to accomplish?

You weren’t kidding, huh.

> Google is less full of crap about the open weights stuff because of Gemma 4, but they are full of crap for a zillion other things I can't exactly feel good about them. So everyone sucks.

Google catching this stray made me laugh, ha.

Pretty much this. I designed my own research harness and infra for theorem proving and conjecturing; however, you still need to review formulations!

Yes, and I use them often in the context of writing adversarial ‘go vet’ style anti-slop analyzers that run pre-commit.

I’ve rolled a small program to enforce consistency, lint rules, and human-authored files for Claude Memory.

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.

Opus 5 broke me; I can’t cognitively deal with Anthropic’s bullshit anymore.

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.

Funny how rule #3 is

> 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?!

Please, no.

> once the sub-matrices get small enough,

the next rabbit hole starts when you try to start lifting F_2 into Z for a given <n,n,n> tensor.

Now, stuff like _this_ is why I keep coming back to HN.

tl;dr CLAUDE_AFK_TIMEOUT_MS=2147483647

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-...

Valid question. If I were further along and had the time to succinctly write up all my contributions, I would just point you at my blog post. I’m generally a poor communicator, so here goes nothing.

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.

My mouth is agape at the fact that this project is basically what I have been working on non-stop for the last three weeks and just yesterday gotten to the point of evaluating; hats off... I only have one novel proof (non-Erdos) and 13 first-time formalizations thus far.

I still like doing maths by pen and paper, but this is fun too.

Even better: you can fork the exeuntu image & make it immediately more relevant to the things you do in addition to just dropping in your programs and such.

I’m shocked I had to scroll this far to find the first sensible reply.

You might be interested to learn I am primarily doing proofs & formal methods.

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.

This is truly vindication for my efforts to get off of frontier models and harnesses as much as possible.

I won't deny the model is _pretty good_ but it is not worth all of this whiplash.

"Fable extended until 26 July" obviously.