I think stuff like "synthetic topology", "synthetic differential geometry", "synthetic computability theory", "synthetic algebraic geometry" are the most promising applications at the moment.
It can also find commonalities between different abstract areas of maths, since there are a lot of exotic interpretations of intuitionistic logic, and doing mathematics within intuitionistic logic allows one to prove results which are true in all these interpretations simultaneously.
I'm not sure if intuitionism has a "killer app" yet, but you could say the same about every piece of theory ever, at least over its initial period of development. I think the broad lesson is that the rules of logic are a "coordinate system" for doing mathematics, and changing the rules of logic is like changing to a different coordinate system, which might make certain things easier. In some areas of maths, like modern Algebraic Geometry, the standard rules of logic might be why the area is borderline impenetrable.
These are more like computational-ish interpretations of sheaves, topological spaces, synthetic geometry etc. The link of intuitionistic logic to computation is close enough that these things don't really make it "non-computational". One can definitely argue though that many mathematicians are finding out that things like "expressing X in a topos" are effectively roundabout ways of discussing constructive logic and constructivity concerns.
I think GIT is a negative answer to a problem originally posed by David Hilbert. It was not proposed by Goedel originally. I think Goedel's main new idea was (i) inventing Goedel numbering (ii) using Goedel numbering to show that provability from a finite FOL signature, and a single FOL formula, is reducible to an equation involving primitive recursive functions (iii) devising a method to translate FOL statements about arbitrary primitive recursive functions into statements about only the two primitive recursive functions + and ×.
Later work establishing the field of computability theory (or "recursive function theory" as it was then known) generalised the insights (i) and (ii). In light of that, Goedel's only now-relevant contribution is (iii).
> When will LLM folks realize that automated theorem provers have existed for decades
This is very misinformed. Automated theorem proving was, sadly, mostly a disappointment until LLMs and other Machine Learning techniques came along. Nothing like the article's result was remotely within reach.
You've confused the mean with the median. GDP Per Capita is not a measure of how well-off the people in a country are.
American states have a lot more income inequality than the UK does, which (due to positive "non-parametric skewness", I think) pulls their GDP Per Capita upwards.
"Even more, this coproduct can be thought of as an instance of a dependent pair indexed by a finite set" - I know what the individual terms mean, but I don't get what this is saying.
A coproduct in the category Set is a disjoint union of sets, i.e. A + B + C where A, B, C are sets.
We can think of this coproduct as involving two choices:
1) a choice of which component of the coproduct we're interested in (first, second, or third)
2) a choice of an element of that component
That is, `A + B + C` is isomorphic to `(i : Fin 3 * D i)` where `Fin 3` is a set with three elements, and `D : Fin 3 - > Type` and
`D(0)=A`, `D(1)=B`, `D(2)=C`.
Then, the idea is: why index by a finite set? If you replace `Fin 3` by some arbitrary set, you start to be able to model a very general notion of a dependent type.
The recent news of multiple solutions to Erdos problem 1196 produced by LLMs without any human help, makes any suggestion that LLMs have hit a wall in reasoning seem less credible. To give you an idea, problem 1196 has been worked on by different experts for years. Now suddenly, LLMs have come along and solved the problem in a multitude of ways. Perhaps LLMs will eventually stall, but this paradigm still has some juice left to squeeze.
But are we talking pure LLMs, or existing AI solvers augmented with LLMs? Because while the latter is impressive, it doesn't state much outside of this specific domain.
If anything, I see greater verticality of specialized software that is using LLMs at their core, but with much aid and technology around it to really make the most out of it.
True, it's an achievement either way. But if an "out of the box LLM" can solve difficult math problems it is an achievement by the LLM vendor. Otherwise it is an achievement by the people doing the vertical integration.
In the context of evolving LLM this is the crucial distinction.
On a tangent: I've tried to connect Euclid's Elements with quantifier elimination theorems. It looks like most of the geometry follows from QE of real-closed fields. Some of the number theory relates to Presburger arithmetic. Some other number theory, including the irrationality of sqrt(2), is down to Skolem. The Pythagorean triples relate to extending Skolem to the Gaussian integers. I suspect some of the "embryonic" integral calculus could be related to holonomic functions, which seem like they admit a form of QE.
Don't have anything for the perfect numbers though.
Let's consider a hash table with an allocation of 1MB, which is about 2^20 bytes. Assume also that each entry occupies a byte. Assuming that the hash function's values are distributed randomly, the probability of there being a collision with only 1000 entries is approximately 38% = 1-(2^20)!/(2^20 - 1000)!/(2^20)^1000. See the "Birthday Problem".
Just about a week ago, Trump was joking about Pearl Harbor on TV while the Japanese PM was sitting right next to him. What's more, she's a nationalist.
I think stuff like "synthetic topology", "synthetic differential geometry", "synthetic computability theory", "synthetic algebraic geometry" are the most promising applications at the moment.
It can also find commonalities between different abstract areas of maths, since there are a lot of exotic interpretations of intuitionistic logic, and doing mathematics within intuitionistic logic allows one to prove results which are true in all these interpretations simultaneously.
I'm not sure if intuitionism has a "killer app" yet, but you could say the same about every piece of theory ever, at least over its initial period of development. I think the broad lesson is that the rules of logic are a "coordinate system" for doing mathematics, and changing the rules of logic is like changing to a different coordinate system, which might make certain things easier. In some areas of maths, like modern Algebraic Geometry, the standard rules of logic might be why the area is borderline impenetrable.
reply