Notoriously, the 737 Max bug that killed a bunch of people was a software patch over a serious mechanical design flaw, and Boeing decided it was easier to make the software engineers fix it than redesign the entire plane.
But it's much better than the prior state of the art which was n^n 2^O(n). [1]
The Quanta article, unfortunately, doesn't bother to report the prior complexity for comparison, despite that that's probably the single most important thing to say in order to support the claim in the article's sub-headline.
LP or ILP? There is a significant difference since for non-discrete problem Linear Programming is shockingly efficient and in no way can be considered a brute force technique.
edit: What would be a technique you consider non-brute force in discrete problems?
I was speculating two oscillators with periods p and q could be composed (as long as there was no way for them to interact) to create an oscillator of period p*q/gcd(p,q) but wondering why large primes wouldn't be a problem.
I think his argument was restricted to a human-produced mathematical result being ported to a Lean program where one would be just as likely to commit a mistake. However I disagree as well, I recall the difficulty of expressing what I wanted to Coq being a barrier to expressing it incorrectly.
The thing about proof checkers is that they won't accept invalid proofs (assuming their internal axioms are consistents...), so if you make a mistake there it will simply reject your proof. The only place where it won't catch some mistakes is in proposition you want to prove, because the only way for it to know what you want to prove if for you to tell it, but that's much easier to humanly verify.
Having worked with a proof assistant is what separates you from Granville (the interviewee in the article). If he had formalized at least a couple of proofs he would not have written things like "people who convert the proof into inputs for Lean". One does not "convert the proof into inputs for Lean" for a simple reason that a proof written in a formal proof language usually contains much more information than the informal prototype. At best one can try to express similar ideas, but it is far from converting a proof from one form to another. If he had formalized a couple of hundred he would have gained a different opinion on the quality of informal proofs as well. A nice list of typical mistakes can be found in this [answer](https://mathoverflow.net/a/291351/163434) to a MathOverflow question.
Good teacher, his Number Theory book felt really good though I have no comparable in Number Theory. I must say Number Theory and Combinatorics are the most difficult topics I got acquainted with in undergrad.
Number Theory is really weird because the definitions and theorems are so often straightforward and easy to understand (you could explain Fermat's Last Theorem to a bright school kid), but the proofs can be devilishly complicated.
Bouty makes excellent chair. Looking at their website I'm thinking Arista/Kadera/Fira. The model of chair I have doesn't seem front page but it is the Sity 9002.
The piston gave after 10+ years of service. Contacted them, warranty is for life, they had someone show up and replace it for free.
F# has diverged quite a lot from OCaml and is very readable IMO.
In any case, I think this view stems from our Algol/c/Java centric CS education system that casts ML and Lisp as weird and “unreadable”, when really it’s just a matter of perspective.
it's really not, in the engineering school I did in the first year we were taught both C and LISP during the same semester and it was obvious to almost everyone except math nerds how much easier C was mapped to a normal human being (e.g. someone without prior programming experience)'s mental model of the world
Someone mentionned in the Mastodon thread that they have an Android phone with nothing-from-google on it. I speculate his installation is even more responsive than whatever default the product came with and I'd like to do that.
I have a terrible Vankyo Z1 table that is very slow. Where do I start?
