Proof assitants have nothing to do with neural nets or optimisation. They are entirely determinitsic and return an absolute "true" or "false" result, not an approximation.
It's not really like that. NN's are only used when searching for new proofs or steps which can be used to fill in details, the verification of a finished proof is done by a classical program by a series of substitutions which are very straightforward and spelled out in detail.
That's not the suggestion. Proof verification is easy (for a proof written in a formal system). Proof search is hard. Many (most/all?) proof assistants heavily use heuristics to guide the proof search. Machine learning on a database of proofs could lead to superior heuristics and make proving stuff in the formal systems easier.
Proving stuff in these systems is still harder than natural language proofs, so making them easier could increase adoption, which would make mathematicians' results more robust/rigorous.
Note that this is editorial license on the part of the writer; Buzzard is proposing the use of interactive theorem provers, which only use a small amount of 80's style AI (backtracking search and higher order matching). No one in ITP is seriously using modern neural net based AI in real theorem provers yet, although there are several research teams working on it.
Curious! Instantiation by means of the language is actually slower than parsing stuff and instantiating the objects that way. Didn't ever think of that possibility before. Anyway, I understand that JavaScript is much more complicated to parse than bare JSON, but still, that just feels odd. Good read!
It looks to be a static site generator. It's surprisingly easy to weather that storm with a simple web server + static sites, it's dynamic sites using Wordpress etc. that have the most trouble.
Not sure if I'm going to express an unpopular opinion on that matter but I'm pretty sure that ot was already said somewhere in the comments in some different form. Not sure if my opinion even counts to people like ones who authored this strange piece of text since I'm from the mischievous and sinister kind of people collectively called "straight white male", and thus I may not have the fitting amount of oppression points to be heard. But I'll try anyway.
I think that the article itself revolves heavily about some prestige or whatever. So here comes the first question: does the person who cares about prestige more than science possess the amount of dedication and discipline to get to the higher ranks? In my opinion, the answer is strong "no" at the very least. To be proficient and productive, to be useful, you have to dedicate all your hard work towards your chosen discipline. Apparently you must be interested very much in it. It doesn't just fall down upon the "privileged cast", it's a competitive field, and outcome of that, if any, depends on dedication and the ability to act smart without relying on anyone or anything else too much.
The second question will be: do you actually know better than the people who make their own life choices? I mean, they do things or don't do them for a reason. Sometimes it's bad, sometimes it's good, but if we talk about education and science, it's nothing close to sexism in the vast majority of cases.
The third part is simpler. What will happen if we enforce/regulate/implement quotas? The amount of useful output will decline. You can't force people into being effective and they will not be effective by "getting there" just by regulations and quotas.
And for the last one, some personal part. Last couple of years I study quite complex math (abstract algebra mostly) on my own out of pure interest in it. I don't have any mentorship, and I don't suffer from it. My dedication compensates for it. It's a bit anecdotal but I believe that you can achieve a lot just by being dedicated and interested. You will not get even close by being placed there and babysat until you're "big enough".
