Not a mathematician, but knowing how proof-checkers work I don't expect them to become practical without some significant future advancement, they certainly aren't right now.
The main problem is that in order to work they have to be connected to the formal definition of the mathematical objects you are using in your proof. But nobody thinks that way when writing (or reading!) a proof, you usually have a high-level, informal idea of what you are "morally" doing, and then you fill-in formal details as needed.
Computer code (kinda) works because the formal semantics of the language is much closer to your mental model, so much that in many cases it's possible to give an operational semantics, but generally speaking math is different in its objectives.
You're commenting on a thread about an interview where an actual Fields medalist explains how proof assistants are actually used to do meaningful mathematical work, today. The issues you raise are all discussed in the interview.
You yourself identified some problems that a modern AI guru would salivate over: Formal specifications from natural language, "filling in" formal details. etc
I'll add another one: NN-based speedups to constraint solvers, which are usually something like branch-and-bound. This is (i've heard) a very active area of research.
The whole article is about Terence Tao predicts it will be practical without a significant breakthrough.
>> I don’t think mathematics will become solved. If there was another major breakthrough in AI, it’s possible, but I would say that in three years you will see notable progress, and it will become more and more manageable to actually use AI.
He think you need another breakthrough to solve mathematics, i.e. making mathematicians obsolete. But even a major breakthrough doesn't happen, AI will be useful for mathematicians in 3 years.
Of course you can still disagree with Terence Tao. He being one of the best mathematicians doesn't make him an oracle.
> But nobody thinks that way when writing (or reading!) a proof
He even very specifically addressed this issue with:
>> Let’s say an AI supplies an incomprehensible, ugly proof. Then you can work with it, and you can analyze it. Suppose this proof uses 10 hypotheses to get one conclusion—if I delete one hypothesis, does the proof still work?
He clearly believes an ugly, incomprehensible proof is much better than no proof at all.
Actually, it is possible to do a high level outline of a proof development and later fill in the details. This is done by starting out with axioms. I.e., don't define the basic types but state that they exist as axioms and also write down their basic properties as axioms. Then later, when you have some development going on, fill in the blanks by turning the axioms into definitions.
I'm not reading it that way, I don't know where you are getting "AI will eventually replace..." from, if anything he seems to have the opposite idea: "even if AI can do the type of mathematics we do now, it means that we will just move to a to a higher type of mathematics".
The line I quoted is in response to "in two to three years mathematics will be “solved” in the same sense that chess is solved".
Unless my priors are dramatically wrong, anyone who believes that is indeed full of shit.
The reasoning is interesting though. I don't necessarily agree with it but it's not "lmao gay".
A posthumous pardon was not considered appropriate as Alan Turing was properly convicted of what at the time was a criminal offence. He would have known that his offence was against the law and that he would be prosecuted. It is tragic that Alan Turing was convicted of an offence that now seems both cruel and absurd—particularly poignant given his outstanding contribution to the war effort. However, the law at the time required a prosecution and, as such, long-standing policy has been to accept that such convictions took place and, rather than trying to alter the historical context and to put right what cannot be put right, ensure instead that we never again return to those times.[0]
> He would have known that his offence was against the law and that he would be prosecuted.
That specific bit of reasoning is very likely wrong.
The circumstances of Turings investigation and arrest started with Turing going to the police to report that had been robbed by a person considered to be a rent boy.
If he had the slightest notion of how homosexual behaviour was dealt with by the regular police and that he would be the main subject of interest rather than the robber he would not have reported the theft.
Turing very much came from a class isolated from common consequences, he spent his youth at an elite school and then university, later at Bletchley Park, all places where lads with an odd bent were not at all uncommon, largely tolerated although often teased, and very rarely, if ever, arrested.
While I find my eyes and ear (même les américaines comprennent) caught by Mme Mac, and I wouldn't have the foggiest in what context "molly with a Dilly" might usually occur, the video and text make one suspect that MM. Doriand and Mika tended to foreground the other characters (do long guns imply rough trade?).
[come to think of it, an odd bent would probably have been a career advantage at Bletchley, in that one might have been already habituated to picking up on metadata during traffic analysis?]
Hell of a tangent, near non contact but, FWiW I pretty sure it's a Sergio Leone film, many of which had sequences shot in Spain and some in North Africa (IIRC) - the blanket toss back is such a trope.
The following piano man bars just prior to the singing are, to my ear, a definite riff on Moby's Extreme Ways that was repurposed for the Jason Bourne films.
They claim that, but I don't see how it could possibly be true, based on the cast listing at https://www.imdb.com/title/tt0056172/fullcredits : apart from an uncredited nurse (Barbara Cole) it seems like a screenplay calculated to make Ms Bechdel sad.
True — I ought to have considered that, for I know the book Seven Pillars of Wisdom has in supertext some passages that (if they made it at all) are probably only referred to in the movie as subtext. mea culpa
Comme je suis bête ! In my defence I saw that one in a 747, so low cabin pressure may not have done my long term memory formation much good. (EDIT: looks like whatever I was remembering as LoA wasn't even that?)
The multivalued functions are a relief — should the sparks/stars lit in my noggin by a comment align in a different direction from intended, it's not that I'm running riot in a deterministic world, but merely finding myself perhaps at the same coordinates, but on a different sheet, in a nondeterministic one?
The Maugham story in which bumble-puppy appears (if slightly later in the decade than in Huxley) is worth reading, especially with the background that WSM worked for MI6 and had (orientation as well as valuation?) reasons to make use of glueings along branch cuts in his personal, as well as his professional, life.
> In a place like the sanatorium where there was little to occupy the mind it was inevitable that soon everyone should know that George Templeton was in love with Evie Bishop. But it was not so easy to tell what her feelings were. It was plain that she liked his company, but she did not seek it, and indeed it looked as though she took pains not to be alone with him. One or two of the middle-aged ladies tried to trap her into some compromising admission, but ingenuous as she was, she was easily a match for them. She ignored their hints and met their straight questions with incredulous laughter. She succeeded in exasperating them.
Being partway through Conflict, War and Revolution(2022)*, I think something may be coming together modelling all your options: Kaczynski and Galois may have been too idealistically violent (the one having done what he could unto others, the other having suffered what he must?) and Grothendieck too idealistically nonviolent (which obviously leads to minimising one's dot product with the world) but Kolmogorov found a nonviolent quadrant inside Machiavelli's pragmatic lead: Fortune provides a martingale process, and virtu consists of minimaxing one's expected interests with respect to her whim.
On a planet like earth it is inevitable that men should seek the favour of Fortune, but it is rarely easy to tell what her feelings are. (or, for that manner, if they even be iid)
For every epsilon of licentiousness, there exists a delta of venus, such that...? (as an algebraist, it seems analysts spend an awful lot of time chasing tails!)
I have been brought up in a culture where seduction follows a sequence ("running the bases"); are there cultures where that does not suffice, and seduction requires more sophistication: a net*, say, or even a filter?
* in line with the genre fiction cover kind of net, someone once won a competition we had at uni for "best line to get a member of the appropriate sex into your room" with 75 pound test, eg https://fr.aliexpress.com/i/839412765.html
No, although I do have a fair amount of shelf space devoted to a CS book series (published by that breakaway technical college somewhere in the fens) all of which are in shades of what I would've called green, but a cantab colleague informed me was in fact blue.
One hint too many! I have been taught that "it's ${LOCATION}ing" is the english equivalent of « il pleuvine », and https://news.ycombinator.com/item?id=40244602 ought to have billions and billions of connections. (none of which involve Leontine S)
(as for me, one of my friends is on the faculty, studying among other things quiver varieties, which brings us full circle back to Penelope, who set up the competition with Odysseus' bow. If it were an asian recurve bow, it makes sense that the suitors might've tried to string it backwards, and if it were a horseback bow, the draw weight for its size might easily have been such that only someone who knew the foot trick for stringing would've managed)
I think the Justice Minister's reasoning is that if we pardon every crime in the past that we deem permissible today, it would legitimize people to break laws they find unjust today, stating that they (perpetrator) did it "because the future will see it as ok". It feels like weak reasoning from my part, but I can't get into the Justice Minister's head. It's just speculation.
With that said, and Turing having been pardoned by the Queen (posthumously), I wonder if pardons in the UK also carry the "imputation of guilt" that pardons in the US carry as defined by the SCOTUS [0]?
Most software developers I know switch to the US layout for coding precisely for this reason. Square brackets are also usually much harder to reach in European layouts, while normally they have a dedicated key.
Personally I use the US layout on all my keyboards all the time, even if it doesn't match the physical keys -- I just can't go back at this point.
Paywalled so I guess I'll never know, but in spite of the scary sounding name the associated press release says the following:
“Despite a large body of evidence from extraordinary efforts by investigators around the world, our committee found that in many cases, if not most, evidence was insufficient to accept or reject causality for a particular potential harm from a specific COVID-19 vaccine,” said committee vice chair Anne Bass, professor of clinical medicine, Weill Cornell Medicine, and a rheumatologist at the Hospital for Special Surgery and New York Presbyterian Hospital. “In other cases, we did find sufficient evidence to favor rejection, favor acceptance, or establish causality. It is important to note, however, that identifying a harm does not mean that it occurs frequently. Harms associated with vaccines are rare.”
Very few proofs in actual professional mathematics are written in a formal proof structure where what you suggest is actually possible. You definitely need to understand the underlying ideas to follow along.
"rewrite in lean when" isn't really practical (at least yet).
Let me clarify: I am not going to waste my time reading the rambling of someone drunk on the AI kool aid.
> profoundly impacted human society,
So far there are fears, well founded fears but any impact is yet to be measured and "profound" has certainly not happened yet.
> driving significant advancements in multiple sectors.
ROTLFMAO. There's nothing more to be said. What is happening is asshole corporate owners destroying their own companies by firing competent workers and replacing them with a bullshit printer. Not quite sure how that's an "advancement".
Bingo. Whenever new coroutines are scheduled to be executed sometime in the future, something somewhere needs to keep them sorted so that the event loop knows how to dequeue them.
It's funny to show this to someone new to CS, but I wouldn't be surprised if you could look at the source for the asyncio implementation and figure out exactly what sorting algorithm you are "actually" using.
Which communist regime has not been nationalist authoritarian? Yes, in theory it is different thing but somehow in practice it always ends up like this.
Well, there is authoritarianism and then there ‘a spy in every phone, internet Great Wall, re-education camps, social credit score’ authoritarianism no?
The main problem is that in order to work they have to be connected to the formal definition of the mathematical objects you are using in your proof. But nobody thinks that way when writing (or reading!) a proof, you usually have a high-level, informal idea of what you are "morally" doing, and then you fill-in formal details as needed.
Computer code (kinda) works because the formal semantics of the language is much closer to your mental model, so much that in many cases it's possible to give an operational semantics, but generally speaking math is different in its objectives.
reply