What is the least flexible version of this tool you’d be willing to pay $20 / month for? Examples:
Graph-To-Matrix Switcher
Paste a small graph or adjacency matrix, hit Translate, instantly see the other form plus the eigen-stuff that often makes the problem trivial. Expectation: no (90%) - thinking “I could flip the representation” is the bottleneck, actually doing it is not a place where tooling is lacking.
Natural language → verified Lean—e.g. user can paste some math they’re working on, LLM tries to translate it into a Lean script and then report back if it was able to do so. Expectation: no (80%) - an LLM chatbot with access to lean checker tool is probably better than any simple-to-build dedicated UI here
Math Clippy for Jupyter notebooks: a sidebar that looks at the current cell, checks if you’re doing anything mathy, and provides hints or links to relevant theorems with a 1 sentence gloss as to why it might be relevant. Expectation: no (80%) - feels like there might be something there that would be useful in the way copilot is useful (i.e. sometimes gets the easy stuff right almost instantly, sometimes is wrong in a way that tickles the user’s brain again almost instantly, in neither case breaking the flow) but I doubt the form factor is right for math
Tex from drawing of equation: user writes out math by hand on a tablet, auto OCR and produce tex, option to hit “accept” and replace selected group of symbols with rendered tex, maybe also very basic error checking of all accepted tex so far. Expectation: yes (75%) but also I expect this already exists.
I’m curious if there are any tools in this space that you keep checking every year or two to see of anyone has built.
What is the least flexible version of this tool you’d be willing to pay $20 / month for? Examples:
Graph-To-Matrix Switcher Paste a small graph or adjacency matrix, hit Translate, instantly see the other form plus the eigen-stuff that often makes the problem trivial. Expectation: no (90%) - thinking “I could flip the representation” is the bottleneck, actually doing it is not a place where tooling is lacking.
Natural language → verified Lean—e.g. user can paste some math they’re working on, LLM tries to translate it into a Lean script and then report back if it was able to do so. Expectation: no (80%) - an LLM chatbot with access to lean checker tool is probably better than any simple-to-build dedicated UI here
Math Clippy for Jupyter notebooks: a sidebar that looks at the current cell, checks if you’re doing anything mathy, and provides hints or links to relevant theorems with a 1 sentence gloss as to why it might be relevant. Expectation: no (80%) - feels like there might be something there that would be useful in the way copilot is useful (i.e. sometimes gets the easy stuff right almost instantly, sometimes is wrong in a way that tickles the user’s brain again almost instantly, in neither case breaking the flow) but I doubt the form factor is right for math
Tex from drawing of equation: user writes out math by hand on a tablet, auto OCR and produce tex, option to hit “accept” and replace selected group of symbols with rendered tex, maybe also very basic error checking of all accepted tex so far. Expectation: yes (75%) but also I expect this already exists.
I’m curious if there are any tools in this space that you keep checking every year or two to see of anyone has built.