chaoxu

I've applied as a team, hope I get in.

Recently I care about how to create harness for mathematics that uses up the complete reasoning ability of the model. I care about both capability and cost.

Most generic harness we have now are not made for maximizing reasoning. I've tested agents like codex, and rarely the cost of reasoning tokens reaches more than 20%. Which is quite strange as math requires a lot of reasoning. So hackathons can be a good test bed.

okey just did some investigation. ~/.config/herdr/herdr.sock JSON-RPC API so we can avoid herdr UI. In fact herdr's TUI is using it too. So basically you can write your own tool to make it work (vibe it with AI if you want)

Something like this would be great. It seems what one really need is just persistent terminal session. So this thing probably can be built on top of zmc with a few scripts.

Herdr did a lot of things really well. It have a great landing page where you can see and interact, and that really made me try it, and a few of my friend was also captured and immediately understood what it is for. I basically do everything remote, never on my own machine.

Once I tried it, I can never go back. It is so simple and worked exactly as I thought how it should work.

I would say it is just a modern version of tmux but really thought about user experience of more novice users. For people who come from the mouse world, moving to this is quite seamless.

Also, coming to the comments, I would think maybe `zellij` would also work well. Or use `zmc` and build something on top. `zmc` is great, as the then the tab/window management can be handled by the desktop or TUI, depend on what someone want to use.

You say hard rules can cause A beats B, B beats C, and C beats A. Is it because hard rules itself can have cycles, or because hard rule and scores together causing cycles? What does tie-breaker even mean here, how does it change the ordering?

Let's ignore tie-breaker. Is it the following abstract problem?

Given a partial order A (the hard rules) and a total order B (the scores). Find a total order C that is an linear extension of A and "agrees" with B the most.

I feel if phrase this way, then there is probably some faster greedy approximation of w/e "agrees" you are thinking about, because w/e you are doing here is also just an approximation of w/e true best you are thinking.

I've always wondered if pandoc can be made reactive. Say markdown to Pandoc AST.

If one changes something, a quick update to the AST would happen incrementally.

Now with all these llm I might actually see if it can be done.

On the webpage's demo, it has a really slick looking UI. How do we have that?

Feels like one can just copy the UI and use it for forgejo. It would get something similar very quickly, and avoid handling all the difficult stuff I guess.

I'm a researcher working in theoretical computer science. Chatgpt found a counterexample of some conjecture I've been trying for 2 years. Also, it one shot many problems I've worked on. It also improved some of my work greatly.

I feel quite useless in the sheer brutal proof writing, counterexample generating skill chatgpt is demonstrating, and wonder what would be the future of my profession.

This is monotone min-plus, so you can do it with even better running time than what you listed (which is just min-plus). Also, if all numbers are at most k, you can even get running time related to k too, replacing n with k is obviously possible, but more can be done too. I feel this might be likely in practice where k might be small?