Am I right that this is a comment on my failure to reply to your previous question in less than 24 hours? I'm afraid I don't look at this website every day. I welcome comments, but it may take me several days to react to them.
With regard to philosophy of mind, one possible elaboration of the point is contained in an earlier post: https://siliconreckoner.substack.com/p/understanding-or-the-computational. Massot is making a claim about "the content" of an idea, specifically that it can be captured indifferently in the form of a logical formula or of a natural language sentence. If this is meant generally then it is a claim in philosophy of mind. To quote the Stanford Encyclopedia article on "concepts":
"disputes about concepts often reflect deeply opposing approaches to the study of the mind, to language, and even to philosophy itself."
Alternatively, Massot is referring exclusively to mathematical ideas. But then he is presuming that these can be meaningfully characterized among ideas in general, which I also see as a claim in philosophy of mind.
Hi Micheal, I generally enjoy Silicon Reckoner but was put off by the tone of your first paragraph. Perhaps I am misreading, but one can read the first paragraph as "look at this sorry (and small) bunch of fools who aren't enjoying the sun and are listening instead to a formal proof from Bourbaki's general topology". I was one of this sorry bunch, really enjoyed the talk, and felt that my excitement afterwards was greater than had I used the time for surfing or tooling down Wilshire Boulevard :)
Re how Massot did it? My understanding is that there is no language model involved. Rather it is a "routine" translation from Lean to English, with a (hand coded) dictionary providing subject specific keywords. The result is almost certainly clunky in places, but I think it would be quite good in general. (I like to think of it as writing in the same way that an inexperienced undergraduate might write, when they first learn how to write a proof: very formulaic, somewhat inflexible, easy to get lost in the thickets of needless detail, but comprehensible for the most part.)
Geordie — thank you for this observation. It wasn't at all my intention to suggest that the crowd was small. I would guess that the audience was typical for an IPAM event and I'm sorry if the first paragraph gave the impression that this is not the case.
Thank you for your answer to the technical question. It's still a mystery to me how the one-to-one translation provides complete and syntactically correct sentences, and I would guess that (as in the third option) the keywords are inserted in the appropriate places in templates (like Mad Libs, if you have that in Australia). I doubt the system has enough templates to accommodate most interesting mathematics.
You may be interested to know that one of the contributors to the AMS Bulletin special issue explicitly predicted that future interactive theorem provers would be integrated with LLMs. The text is still being edited so I can't say more.
The larger point is that Massot's offhand assertion that "the content is the same" is neither self-evident nor innocent. It is a strong and highly questionable metaphysical claim that attempts (but necessarily fails) to short-circuit fundamental controversies not only in philosophy of mathematics but in philosophy of mind.
Michael, what I know of Mathematics beyond undergraduate level can be fit into a size 6 Homburg, but I do know somewhat about the philosophy of Mind, can you expand on your last referral to it?
Well it would have been nice...
Am I right that this is a comment on my failure to reply to your previous question in less than 24 hours? I'm afraid I don't look at this website every day. I welcome comments, but it may take me several days to react to them.
With regard to philosophy of mind, one possible elaboration of the point is contained in an earlier post: https://siliconreckoner.substack.com/p/understanding-or-the-computational. Massot is making a claim about "the content" of an idea, specifically that it can be captured indifferently in the form of a logical formula or of a natural language sentence. If this is meant generally then it is a claim in philosophy of mind. To quote the Stanford Encyclopedia article on "concepts":
"disputes about concepts often reflect deeply opposing approaches to the study of the mind, to language, and even to philosophy itself."
Alternatively, Massot is referring exclusively to mathematical ideas. But then he is presuming that these can be meaningfully characterized among ideas in general, which I also see as a claim in philosophy of mind.
Hi Micheal, I generally enjoy Silicon Reckoner but was put off by the tone of your first paragraph. Perhaps I am misreading, but one can read the first paragraph as "look at this sorry (and small) bunch of fools who aren't enjoying the sun and are listening instead to a formal proof from Bourbaki's general topology". I was one of this sorry bunch, really enjoyed the talk, and felt that my excitement afterwards was greater than had I used the time for surfing or tooling down Wilshire Boulevard :)
Re how Massot did it? My understanding is that there is no language model involved. Rather it is a "routine" translation from Lean to English, with a (hand coded) dictionary providing subject specific keywords. The result is almost certainly clunky in places, but I think it would be quite good in general. (I like to think of it as writing in the same way that an inexperienced undergraduate might write, when they first learn how to write a proof: very formulaic, somewhat inflexible, easy to get lost in the thickets of needless detail, but comprehensible for the most part.)
Geordie — thank you for this observation. It wasn't at all my intention to suggest that the crowd was small. I would guess that the audience was typical for an IPAM event and I'm sorry if the first paragraph gave the impression that this is not the case.
Thank you for your answer to the technical question. It's still a mystery to me how the one-to-one translation provides complete and syntactically correct sentences, and I would guess that (as in the third option) the keywords are inserted in the appropriate places in templates (like Mad Libs, if you have that in Australia). I doubt the system has enough templates to accommodate most interesting mathematics.
You may be interested to know that one of the contributors to the AMS Bulletin special issue explicitly predicted that future interactive theorem provers would be integrated with LLMs. The text is still being edited so I can't say more.
The larger point is that Massot's offhand assertion that "the content is the same" is neither self-evident nor innocent. It is a strong and highly questionable metaphysical claim that attempts (but necessarily fails) to short-circuit fundamental controversies not only in philosophy of mathematics but in philosophy of mind.
Michael, what I know of Mathematics beyond undergraduate level can be fit into a size 6 Homburg, but I do know somewhat about the philosophy of Mind, can you expand on your last referral to it?