Viewing profile — mmaaz

great q! there's a variety of levers here. for one, it uses newton polytope pruning to prune the monomial basis -- this often helps a lot in practice, especially for sparse polynom…

Current support for nonlinear inequalities in Lean is quite limited. This package attempts to solve this. It contains a collection of Lean4 tactics for proving polynomial inequalit…

Really cool work!

Very cool!

To provide some additional context: the algorithm being used by QEPCAD is cylindrical algebraic decomposition, which has a time complexity 2^2^n (yes, doubly exponential). So, whil…

this is really brilliant!!

This website showcases our agent, based on Claude, that autonomously infers properties of code and tests them using Hypothesis. Our agent found hundreds of bugs across popular Pyth…

Exactly the same here, late night would be my most productive. I don’t know how sustainable this is as I mature lol.

Tbh the code I was writing wasn’t that complex from an engineering perspective. During my PhD I was writing “research code” which is more like writing scripts, not a full blown app…

Wow, I feel for you, that sounds really scary. Honestly no, I’ve scarcely changed how I work, except for being more strict about keeping a rigid schedule, forcing myself to take br…

Hmm not sure what you mean. In the case of MOGAD, it actually attacks the lining of the nerve. The MOG means myelin oligodendrocyte glycoprotein, which is a protein in the myelin s…

Good advice. I didn’t have a stroke but a couple months ago I developed blindness in my left eye. It came down to my optic nerve being inflamed. I was later diagnosed with a rare a…

Some time ago, I was on a team of researchers collaborating with a hospital to build some ML models for them. I joined the project somewhat late. There was a big fuss over the fact…

I love this as someone who used to work on max-weight matchings and now works on LLMs :)

Fascinating insight into the industry. Thanks for sharing.

Curious what you mean by this. Do you mean like an AlphaEvolve type thing?

The state of the art solvers are the proprietary ones like Gurobi, FICO, Cplex, Mosek, etc. A major contributor to the proprietary "sauce" is in the heuristics they use. For exampl…

I tried it with a certain conceptual problem in computer algebra (which I’ve had dismal results on GPT o1-preview and o1-mini… sort of a private benchmark) and it spent 2 minutes a…

I think this is a criticism about the general Python ecosystem, but the article has nothing to do with what other package authors do or security vulnerabilities etc. It converts SA…