Hacker News: mmaaz

New comment by mmaaz in "Show HN: Sostactic – polynomial inequalities using sums-of-squares in Lean"

mmaaz — Tue, 21 Apr 2026 18:53:34 +0000

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 to pass degree bounds in the case of a ratio of SOS, as well as a template for the denominator (e.g., ax^2 + ay^2), which also cuts down on the monomials, as well as possibly introducing affine constraints tying coefficients together. of course, in the positivstellensatz case, you can also specify the degree bound.

I wrote about all these tricks here https://mmaaz.ca/writings/sostactic.html.

and yeah, there is a clli interface for the python backend, the lean interface calls the cli.

Show HN: Sostactic – polynomial inequalities using sums-of-squares in Lean

mmaaz — Sat, 18 Apr 2026 22:36:33 +0000

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 inequalities via sum-of-squares (SOS) decompositions, powered by a Python backend. You can use it via Python or Lean.

These tactics are significantly more powerful than `nlinarith` and `positivity` -- i.e., they can prove inequalities they cannot. In theory, they can be used to prove any of the following types of statements

- prove that a polynomial is nonnegative globally - prove that a polynomial is nonnegative over a semialgebraic set (i.e., defined by a set of polynomial inequalities) - prove that a semialgebraic set is empty, i.e., that a system of polynomial inequalities is infeasible

The underlying theory is based on the following observation: if a polynomial can be written as a sum of squares of other polynomials, then it is nonnegative everywhere. Theorems proving the existence of such decompositions were one of the landmark achievements of real algebraic geometry in the 20th century, and its connection to semidefinite programming in the 21st century made it a practical computational tool, and is what this software does in the background.

Comments URL: https://news.ycombinator.com/item?id=47820134

Points: 14

# Comments: 1

New comment by mmaaz in "Gaussian Splatting – A$AP Rocky "Helicopter" music video"

mmaaz — Mon, 19 Jan 2026 09:44:52 +0000

Really cool work!

Finding bugs across the Python ecosystem with Claude and property-based testing

mmaaz — Wed, 14 Jan 2026 23:19:20 +0000

Article URL: https://red.anthropic.com/2026/property-based-testing/

Comments URL: https://news.ycombinator.com/item?id=46625428

Points: 1

# Comments: 0

New comment by mmaaz in "Total monthly number of StackOverflow questions over time"

mmaaz — Sun, 04 Jan 2026 04:01:50 +0000

Very cool!

New comment by mmaaz in "Slaughtering Competition Problems with Quantifier Elimination (2021)"

mmaaz — Tue, 30 Dec 2025 02:45:49 +0000

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 into CAD, this is often not tractable. This isn’t a knock against CAD: imo it is one of the most fundamental and under-appreciated algorithms and I devoted a big chunk of my PhD thesis to it.

By the way, to my knowledge QEPCAD is essentially the only complete open-source implementation of it. Mathematica also implements it. I wrote one of the few open-source implementations of it, although it does not do quantifier elimination; it only returns the truth of a given statement. https://github.com/mmaaz-git/cad.

New comment by mmaaz in "Algorithms for Optimization [pdf]"

mmaaz — Mon, 01 Dec 2025 06:49:52 +0000

this is really brilliant!!

Mathematics is hard for mathematicians to understand too

mmaaz — Thu, 27 Nov 2025 23:05:54 +0000

Article URL: https://www.science.org/doi/10.1126/science.aec9014

Comments URL: https://news.ycombinator.com/item?id=46073978

Points: 134

# Comments: 148

New comment by mmaaz in "Agentic Property-Based Testing: Finding Bugs Across the Python Ecosystem"

mmaaz — Tue, 18 Nov 2025 08:25:05 +0000

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 patched! On this website, you can browse all of the bugs it found. You can read the linked paper and code for more information.

Agentic Property-Based Testing: Finding Bugs Across the Python Ecosystem

mmaaz — Tue, 18 Nov 2025 08:25:05 +0000

Article URL: https://mmaaz-git.github.io/agentic-pbt-site/

Comments URL: https://news.ycombinator.com/item?id=45962684

Points: 2

# Comments: 1

New comment by mmaaz in "Tips for stroke-surviving software engineers"

mmaaz — Thu, 30 Oct 2025 06:47:49 +0000

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

New comment by mmaaz in "Tips for stroke-surviving software engineers"

mmaaz — Thu, 30 Oct 2025 06:46:23 +0000

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 translating the math/algorithms to code. And I would just get into a flow state sometimes and could not stop haha. I had a (bad?) habit during my PhD that whenever I was stuck on a problem I just kept bashing my head against it until I solved it (code or math).

New comment by mmaaz in "Tips for stroke-surviving software engineers"

mmaaz — Thu, 30 Oct 2025 06:42:45 +0000

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 eye is totally fine. But I do feel the eye strain come on sooner from relying on one eye.

New comment by mmaaz in "Tips for stroke-surviving software engineers"

mmaaz — Thu, 30 Oct 2025 06:39:23 +0000

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.

New comment by mmaaz in "Tips for stroke-surviving software engineers"

mmaaz — Wed, 29 Oct 2025 06:42:01 +0000

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 nerve. Thankfully my vision is approx 95% recovered by now. But I still can’t read, eg code on my laptop, which is scary (my right eye is basically making up for it). And I’m scared of another attack happening. So I’ve been really looking after my health and trying not to do the 12+ hr coding benders I used to do. I appreciate these tips!

New comment by mmaaz in "You already have a Git server"

mmaaz — Mon, 27 Oct 2025 05:24:19 +0000

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 internet, so the researchers couldn't use GitHub, so they had been stalled for months. I told them that before GitHub there was `git`, and it is already on the servers... I "set up" a git system for them.

New comment by mmaaz in "Ask HN: What are you working on? (October 2025)"

mmaaz — Mon, 13 Oct 2025 07:12:28 +0000

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

New comment by mmaaz in "Why did Crunchyroll's subtitles just get worse?"

mmaaz — Tue, 07 Oct 2025 06:39:43 +0000

Fascinating insight into the industry. Thanks for sharing.

Property-based testing of batch-invariant operations

mmaaz — Sun, 05 Oct 2025 22:53:01 +0000

Article URL: https://www.mmaaz.ca/writings/batch-invariance.html

Comments URL: https://news.ycombinator.com/item?id=45486002

Points: 1

# Comments: 0

New comment by mmaaz in "Integer Programming (1977) [pdf]"

mmaaz — Tue, 09 Sep 2025 06:23:04 +0000

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