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.

I care. I was a math student in my undergrad when I try to solve a particular problem on paths, in the end it uses a path version of cycle double cover conjecture (which was solved in the 90s).

https://chaoxu.prof/posts/2013-01-30-there-exist-a-path-of-l...

I also want to get it to work on cycles, but then I hit the cycle double cover conjecture so I gave up.

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?

My version of a WYSIWYG built on top of CM6.

https://github.com/chaoxu/coflat

Mine also have lot of bugs (especially reader and editor doesn't completely match yet).

repro the issue: click random places and add random texts, scroll around, and issues come up sooner or later.

I'm testing it and seems to be very broken, typing things around and things jumps everywhere.

I was trying to create something like this too, because I need something that also work for mathematical writing. Let me push a version on github and update, it fixes a lot of issues.

Unfortunately it works on my own version of markdown, which is a subset of pandoc markdown, but I think one can get claude to update the parser to work for other things.

I’m really interested in AI4MATH, as I believe it will eventually replace me.

I'm working on a mathematical knowledge base software.

It's kinda like a local Github for math. In fact the backend is actually a Forgejo instance, I'm building a frontend for human and also a harness for agents that automatically consumes the knowledge base and expand on it. I realized the Issue/PR/review workflow works well for maintaining knowledge base too.

The motivation is actually help mathematicians/me TODAY to able to do math together with human/AI.

The knowledge base keeps mathematical writing as plain Markdown, but adds stable IDs, backlinks, search, draft changes, review, approvals, and merge. The agent side can read the same pages, follow the same references, propose edits, and go through the same review process as a human.

I’m not using formalization here. Everything is still natural-language proofs. The practical reason is that many areas I care about are not easy to formalize yet because it is not in mathlib.

I see this as a transition project: useful before autoformalization really works well, and maybe still useful afterward as the place where humans and agents organize exploration.

I can’t read it at all on mobile because I can’t scroll down. Is there a summarization?

> Because frankly nobody gives a sh about throwing resources and finding just better (not globally optimal) solutions to synthetic benchmarks.

This does not align with my experience of people working in OR.

A heuristic using problem specific structure can beat Gurobi which is for solving general mip.

Just tried it. Does it support theorem environments?

Many LaTeX tricks only get passed down from advisors to students, or from collaborators to collaborators. Rarely someone would look for how to improve their typesetting when all they want is to quickly communicate content.

It be nice if content and typesetting can be completely separated, where I just write content, and something (LaTeX, AI, some manual typesetter) does all the typesetting.

Also, should I be the one controlling how the reader consume my content? Maybe the reader prefers another font? Or the reader is viewing in a kindle so pdf page size should be different?

This would be impossible unless the reader have my LaTeX source code and compile it themselves. But it is super simple for epub, or html webpage (by modifying the css).

How is Quarto? It uses Pandoc Markdown.

Have you tried Quarto? It should tick everything in your box (except MathML, but hey that might work too since Quarto is built on pandoc)

What if we only tax luxury goods?

It looks really nice! I’ve sent this to a few friends to check it out.

To give some context, I'm a professor in theoretical computer science, so I write a lot of LaTeX documents and notes.

Some observations of my work flow.

  - Writing: I'm writing the source, and occasionally look at the output. So as long as the output time is reasonable, then it is sufficient. 
  - Editing: I'm reading the output, and then edit the source. So going from the output to the part of the source I have to edit should be as smooth as possible. 
  - Typesetting is the least of my concern. I only check if there are any glaring typesetting problems right before we publish. This takes at most 1% of the total time in preparing a document. 
  - Live editing almost never happen. But I see why it might be useful to incorporate it into the work flow. (A cursor on the rending of the live editing would be very nice)

There are some choices on how to present source and the rendering.

Typst went with the 2 panel design, with one side source, one side rendering. So I found something close to WYSIWYG is better for editing. However, full WYSIWYG is hard to get right and comes with its own problem. Currently I found there are a few common things people do with respect to source/rendering.

  - WYSIWYG editors, which renders everything (word, TeXmacs, Lyx). Editing is done in the rendering. It is smooth, but takes a long time to get used to.
  - The app Typora that renders everything except the part where you are editing (which shows as the source). This can be generalized to render all except the current line, or something similar. Editing is done in the source, but feels like I'm editing in the rendering. This is extremely smooth for my editing work, and is my preferred way. 
  - The app like Compositor https://compositorapp.com/ that renders everything, but can call out the selected part of the source. 
  - The source and render are in two different panels. Editing is done in the source. So usually one can click part of the rendering, and cursor jumps to the corresponding part of the source. This introduce some friction, as the eyes have to do a jump, and also a quick context switch.

I understand this is useful for people who doesn't type math regularly, but as someone who write a huge amount of math, `$...$` is so much less friction than the LaTeX one `\(...\)`.

Even in LaTeX, mix and match. `$...$` for normal mode, and `\[...\]` for display math, and it works well for two reasons. Inline math are generally short, less prone to mistakes, so `$` saves a lot of time.

Recently I have been testing vditor, vditor is a markdown editor that have a instant rendering feature [1]. If I'm creating my own editor, how hard is it to implement it using Lexical?

[1] https://github.com/Vanessa219/vditor/blob/master/README_en_U...

This is true.

But how does someone take advantage of it without changing their current behavior: write an entire paragraph and do 2 line breaks.

Always end a sentence with '.\n'? Manually format lines so no line have more than 80 characters?

Oh this feature is great. Solves my problem completely.

I wish github would also implement word-diff option.

Edit: Github actually does some form of word-diff! See example here: https://github.com/chaoxu/chaoxu.github.io/commit/6d9ab6eefc...

I also looked up how word-diff work with Chinese language. Found a useful stackoverflow link with other suggestions.

https://stackoverflow.com/questions/26135133/git-word-diff-o...

git is line based, so good for code.

But not for most markdown files, at least how I use it. I only start new line (actually, 2 new lines) when I reach a new paragraph, and I think this is normal for most people who ever write something in markdown.

So now I get a huge 2000 character line with a few small edits, and I can hardly see where the changes are.

I wonder if one can hollow out the individual cubes to decrease the weight.

I actually don't get why corporation should pay taxes. When the profit of the company is distributed, or paying the employees, the employees/shareholders will be taxed on that money.