Thanks! I’m glad you enjoyed it. You may also get a kick out of the YouTube hyperlinks in the GitHub readme, especially the advanced methods for establishing convexity one :)
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.
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!
Even when I was young, I discovered that after a certain level of fatigue my coding became garbage, and after a night's sleep I had to delete it and redo it. After this tipping point, I just stop doing the hard stuff. If I still want to work, I work on routine things that didn't take much concentration.
I never understood how people can write complex code when fatigued. I just get negatively productive trying that.
> I discovered that after a certain level of fatigue my coding became garbage, and after a night's sleep I had to delete it and redo it.
My best work happens at 2am, at about 4am I am too tired and get slow and get stuck, I think even then code quality suffers only a little bit.
That's just my experience, I believe it happens because if I am working at that time, I am hyped and or in the zone. There is a sort of second wind involved. The lack of distractions also helps I guess.
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).
Thanks for sharing! I feel the fear of another attack with epilepsy too. It is terrifying. The doom and the walking on thin ice constantly hoping you're not gonna over-step or do the wrong thing. And all that at the same time as trying to live your life fully. Do you have any devices or aid software to help with the not-reading thing? I imagine it's all really fresh still and you're just taking it a day at a time?
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.
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.
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.
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" phase which attempts to eliminate redundant constraints/variables. There may be some ML they are using behind the scenes to derive these heuristics, I'm not sure, although I know it is a major research area.
Otherwise, the basic underlying algorithms are all the same, as in the textbook: branch-and-bound and so on.
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.
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 packages and dependencies that map back to the SAT instance. And it’s definitely just for fun, I highly doubt it’s useful except as an exercise in NP-complete reductions :)
