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.
I would have loved to have had ChatGPT when I had to do a few modules in formal methods, I'd say it would have eaten through the BS I had to wade through
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?
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 was able to repro one issue that could have been contributing to your broken experience - there's a slight delay between, for example, clicking text in a heading and having the "#" markdown decoration appear. This is to prevent the mouse location from shifting mid-click and causing text to be selected unintentionally (obsidian does this too). But there was a bug that was causing a cascading set of failures if edits happened during that delay window, which is likely what folks who are clicking around at random points in the editor and adding text are doing. I fixed it in 0.4.2, which should be live now.
Thanks for trying it out! would you mind giving some steps that allow me to repro the issue? It's early days so i'm sure there are some rough edges, hopefully I can fix them quickly.
I just clicked around a bit and randomly typed, suddenly no matter where I typed, my text was ending up at the end of the document. Found it to be pretty broken as well.
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.
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).
To a certain degree, the LaTeX environment is already like that. I designed my custom resume style years ago and rarely touch it. I often tweak the actual content which gets poured into the style to produce the final document. The few changes I’ve made to the style have never affected the (separate) content either.
> Many LaTeX tricks only get passed down from advisors to students, or from collaborators to collaborators.
Which is a great point on why the average quality of LaTeX homework submissions by undergraduates without any research experience usually makes for a less-than-ideal grading experience. And this is not about the nit-picky mistakes, but the visually glaring ones.
> 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).
Well ..., wouldn't the html page be the source code in this case? Also, in most cases changing the look of a LaTeX document is as simple as changing the docuent class or switching to a different package. Also, modifying CSS is anything but simple in some cases, especially when the original style is not ideal.
reply