mmaaz

8 ms·

1.
by mmaaz 5mo ago
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 polynomials. also, both the lean and python interfaces allow t
2.
Show HN: Sostactic – polynomial inequalities using sums-of-squares in Lean(github.com)
14 points by mmaaz 5mo ago|1 comments
3.
by mmaaz 8mo ago
Really cool work!
4.
Finding bugs across the Python ecosystem with Claude and property-based testing(red.anthropic.com)
1 points by mmaaz 8mo ago|0 comments
5.
by mmaaz 9mo ago
Very cool!
6.
by mmaaz 9mo ago
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, while in theory many problems could be solved by tossing them in
7.
by mmaaz 10mo ago
this is really brilliant!!
8.
Mathematics is hard for mathematicians to understand too(science.org)
134 points by mmaaz 10mo ago|148 comments
9.
Agentic Property-Based Testing: Finding Bugs Across the Python Ecosystem(mmaaz-git.github.io)
2 points by mmaaz 10mo ago|1 comments
10.
by mmaaz 10mo ago
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 Python libraries, some of which we have since reported and patch
11.
by mmaaz 11mo ago
Exactly the same here, late night would be my most productive. I don’t know how sustainable this is as I mature lol.
12.
by mmaaz 11mo ago
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 application or library. The most challenging part was translati
13.
by mmaaz 11mo ago
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 breaks, etc. It’s only my left eye that can’t read, the right
14.
by mmaaz 11mo ago
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 sheath.
15.
by mmaaz 11mo ago
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 autoimmune condition called MOGAD which “attacks” the optic n
16.
by mmaaz 11mo ago
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 that the hospital servers were not connected to the interne
17.
by mmaaz 11mo ago
I love this as someone who used to work on max-weight matchings and now works on LLMs :)
18.
by mmaaz 1y ago
Fascinating insight into the industry. Thanks for sharing.
19.
Property-based testing of batch-invariant operations(mmaaz.ca)
1 points by mmaaz 1y ago|0 comments
20.
by mmaaz 1y ago
Curious what you mean by this. Do you mean like an AlphaEvolve type thing?
21.
by mmaaz 1y ago
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 example, all solvers will have a "presolve" ph
22.
by mmaaz 2y ago
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 arguing with itself about what a Python function was called.
23.
by mmaaz 2y ago
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 SAT to “dependency resolution” by creating a bunch of dummy pa
24.
by mmaaz 2y ago
On that note, uv, which I found to be orders of magnitudes faster (pip fails to solve even some small SAT/IP instances) uses something called PubGrub https://docs.astral.sh/uv/reference/resolver-internals&#x2F
25.
by mmaaz 2y ago
Thanks!
26.
Solving Boolean satisfiability and integer programming with Python packaging(mmaaz.ca)
77 points by mmaaz 2y ago|25 comments