Through statistics you could do this but it would be alot of effort. My father used to assign a point system to his favorite wars (the two opposing sides). The more intricate and elaborate the research the closer the point system is to the truth. Computer software uses AI in this way. Much of AI is built using data mining techniques. Many online forums are used for data mining especially facebook. How does that relate to the OP is that if you put enough effort into any given subject you can approach a problem with a scientific backing.

One way could be by measuring the impact of given theorem in terms of application, practical or theoretical. Consider a theorem x. If it's applicable in a large number of fields in math, science, sociology, etc. then it proves itself to be an interesting theorem doesn't it? Surely we can invent a point-scoring system based on my proposal. Unfortunately that's as far as I can go since I'm not a mathematician but a big fan of it, yes.

Something interesting needn't be a theorem too. It could be just a number. I don't know how reliable youtube is but there's a claim that the number 0.577 (Euler-Mascheroni constant) is "very" interesting because it pops up in many areas of science and people, as of yet, haven't figured out why.

First off you’d have to examine what ‘interesting’ means and the kinds of features present in ‘theorems’ that are tells of interest.

From there you could probably come up with a roughshod means of measure.

I'm not sure about a function, but the number of results that depend on a given result might be a possible metric.

So at the bottom of an inverted dependancy pyramid would be the fundamental axioms of maths, above that the most fundamental theorems and above that, the base of the pyramid, would be newly invented theorems.

Yeah. If you're paying it attention, it's of interest to you.

Yeah. If you're paying it attention, it's of interest to you. — Shamshir

:rofl: :up:

Well, what I meant to ask was is if could exist (or if somebody invented) any "automatic" and "objective" way to recognize meaningful mathematical theorems (or theories) when they are expressed in a formal language.
Probably the answer is NO. But if there is no such thing as an objective "value" of a mathematical sentence, how can mathematicians be able to recognize an "interesting" new theory when they see one?

If you take Google Scholar citations for math papers as a directed graph then use some measure of centrality (like an Erdos number), you'd get a measure of citation influence for papers. Whether this maps onto interest is a different question.

My question is: is there a sensible way to define a measure how 'interesting' is a given theorem (or theory)? — Mephist

In my impression, we would need a function F that returns the a priori likelihood that any arbitrary theorem s is provable from theory T. From there on, we can use Shannon information theory to compute the surprisal, i.e. the information content, i.e. the self-information of the message that says that s is indeed provable from T. We could simply use proof P as the message here.

So, a simple strategy consists in constructing the best possible software program that tries to look up the existing proof for any arbitrary, given theorem. If the program can locate this proof, then there is no surprise attached to the fact that the theorem is provable, and then the theorem is not particularly interesting. If the program cannot locate the proof, but you still manage to supply it, then your theorem actually is interesting.

we can use Shannon information theory to compute the surprisal, i.e. the information content — alcontali

Isn't that mainly used in compression algorithms? Like, given a 'q' the odds of the next letter being 'u' is 99%, or something like that. Where we see it every day (or minute) is in data compression. The point of it was to reduce redundancy or transmit the maximum amount of information in the minimum number of bits. So how could that be applied in such an abstract 'possibility space', so to speak?

So how could that be applied in such an abstract 'possibility space', so to speak? — Wayfarer

Yeah, that is why a highly simplified strategy is easier to implement. Check if the theorem is already known to be provable, and then it is not interesting. It is only interesting to the system, if the system cannot determine if it is provable, but you manage to supply the proof. All existing known provable theorems are then considered boring by the system.

I don’t know but i think work on measuring abstract human concepts like how interesting, original, artistic, aesthetic and so forth things are should be useful in the work on developing artificial intelligence. But I also suspect it too will suffer from what psychology and ethics suffer from, which is that are rather vague, and what humanities suffers from, which is that they’re rather generalising and socio-political, or what formal logic suffers from, which is that it’s rather dismissive of plain common sense (which, though sometimes prone to irrationality, is often very useful). Not to mention the direction of research on AI always being on leash of commercial interests, political beliefs, and even culture, technically difficult and technologically bottlenecked as it already is.
But I don’t think there is a better approach to this than plain old Utilitarianism schemed into an object-oriented computer framework, but with lots of room for approximation and error (of judgment?) in the parameters and variables.
But it is perhaps advisable to remember that all of that will always incorporate and be incapsulated by the human side of things, and won’t become a proper sovereign and intelligent entity, simply because computers are invariably built by humans, according to an intelligent design and for a certain purpose, unlike us humans who seem to have come from a sort of accidental freak-whim of nature for reproduction and evolution, nature itself also being a freak-whim of...something (Supernature? Bearded guy is the heavens? Mysterious strings? Nobody knows). People and their minds, quite different things from laptops and their Microsoft Windows.

Well, first of all, I am happy that finally somebody considered my question interesting :smile:

I actually have a quite different opinion about this: I think that provability, or how easy is it to find a proof, has nothing (or very little) to do with the fact that the theorem expresses an interesting mathematical proposition. But I agree with you that some kind predictability measure (such as the one defined by Shannon information theory) should have a role.
My opinion is that the essential information is not in the theorem itself, but in it's "interpretation" on the mathematical model that we have in mind. In fact, I believe that even if you took a very talented mathematician that has no knowledge at all about a new theory, and you presented him with the purely formal expression of a theorem, he wouldn't be able to say if that is something interesting or absolutely boring. In fact there are several cases in the history of mathematics of original results that were completely ignored at a first time, and then become very important after several years from their publication: one famous example is Galois' group theory.
So, from this point of view, the representation of a theory in Category theory as a functor from the logical proposition to the the model should be the object that is taken into account to calculate Shannon's probability. And in my opinion there exists an objective way to define such a function in a way that matches very closely what mathematicians consider to be the degree of "interest" of a theory. And that, of course, would be essential to build some kind of A.I. software that "understands" mathematics.

I don’t know but i think work on measuring abstract human concepts like how interesting, original, artistic, aesthetic and so forth things are should be useful in the work on developing artificial intelligence — Frotunes

Yes, I agree.

But I also suspect it too will suffer from what psychology and ethics suffer from, which is that are rather vague, and what humanities suffers from, which is that they’re rather generalising and socio-political, or what formal logic suffers from, which is that it’s rather dismissive of plain common sense (which, though sometimes prone to irrationality, is often very useful) — Frotunes

Well, I believe mathematics is a different case in this regard: I think that the degree of "interest" of a theory can be defined, somehow similarly to how the degree of "randomness" of a number has been defined.

Hmmm..I doubt it but ok.

But I agree with you that some kind predictability measure (such as the one defined by Shannon information theory) should have a role. — Mephist

Yes, I agree. Furthermore, we do not really need to solve the problem.

We would only need to show some progress, and give them impression that the approach is possibly promising.

That could actually be enough for writing a grant proposal and get funding to do some work on the problem. There are institutions that actually pay for this kind of stuff. If you manage to remotely justify why they should hand over resources from their precious budgets, they may even do it.

In fact, I believe that even if you took a very talented mathematician that has no knowledge at all about a new theory, and you presented him with the purely formal expression of a theorem, he wouldn't be able to say if that is something interesting or absolutely boring. — Mephist

If you look at the set of axioms A of a theory T and then at a theorem S that is provable from T, the surprise is probably related to some concept of distance d(S,A). The longer the distance, the more surprising, I guess.

It also depends on the existence of other known provable theorems S1,S2,..., and the distance d(S,S1), d(S,S2), and so on. If d(S,S[k]) is large for each known-provable S[k], then theorem S could be deemed "interesting".

So, maybe we could try to develop a notion of theorem "distance"?

It has to be some kind of "shortest distance", because otherwise, people could make their theorems more interesting just by adding otherwise useless steps in their proof.

o, from this point of view, the representation of a theory in Category theory as a functor from the logical proposition to the the model should be the object that is taken into account to calculate Shannon's probability. — Mephist

Yes, we could consider necessary non-superfluous steps in the proof to be a concept for distance, and hence somehow some kind of proxy for Shannon probability?

And that, of course, would be essential to build some kind of A.I. software that "understands" mathematics. — Mephist

Maybe some kind of plugin or script for Coq or Isabelle?

Well, what I meant to ask was is if could exist (or if somebody invented) any "automatic" and "objective" way to recognize meaningful mathematical theorems (or theories) when they are expressed in a formal language.
Probably the answer is NO. But if there is no such thing as an objective "value" of a mathematical sentence, how can mathematicians be able to recognize an "interesting" new theory when they see one? — Mephist

The probability of the answer being "No" is 1.

"Interesting" is a judgment that an individual makes.

Sometimes it seems to me that there are people who don't understand how they can make judgments about anything. Maybe there's some medical condition that makes judgments difficult or even absent?

Actually, I changed idea about the "No" answer since i wrote that post :razz: (2 months ago)

I think that the case of mathematics is quite different from judgments on subjects such as, for example, music or literature.

In fact, I believe that between mathematicians that work on a given theory there is quite unanimous consensus on which theorems are the most important ones.

There are of course lots of people thinking that the whole subject of mathematics is not interesting at all. But between the group of people that understand a given theory, the definition of "interesting" can be very often (if not always) translated to "surprising", or "improbable coincidence". And that's the kind of judgment that, in my opinion, can be "measured" in an objective way.

Of course there will be people that disagree with this "measure", but we have a quite objective test for how good this measure would be: the history of mathematics is full of theorems that have been discovered and then forgotten, because judged irrelevant, and a very few of them that have been studied in schools for hundreds or even thousands of years.

You could make it, "Is it possible to develop a heuristic that can predict widespread consensuses about what's interesting, at least within a limited milieu?" That might work for some milieus, like mathematics, as you note.

But the "it's interesting" part is still not objective/it's still a matter of individual judgment.

OK, probably you are right: my question was too generic and didn't express what I wanted to mean.

Let me give you some simple examples of theorems taken from here: http://www.cs.ru.nl/~freek/100/ to illustrate my idea of "probability measure" for a theorem.


1. Pythagorean Theorem

- Theorem expressed in a formal language: (Theorem number 4 from https://madiot.fr/coq100/)

Theorem Pythagore :
forall A B C : PO,
orthogonal (vec A B) (vec A C) <->
Rsqr (distance B C) = Rsqr (distance A B) + Rsqr (distance A C) :>R.


From a formal point of view, it's a logical equivalence between orthogonality of two vectors and an equation between real numbers (vectors' lengths).

Should an equivalence of this kind be surprising? (or improbable)? The answer is NO: in fact, whatever angle you take between two vectors, there will be an induced equation between vectors' lengths, and vice-versa.

So, why do you find the theorem surprising when you read it for the first time if you didn't know it before? (if you understand it)
Because it's a coincidence between two special cases:
- orthogonality is a special case of angle between vectors (a very particular one: the length of the projection of one vector on the other is zero)
- the sum of squares is a special case of equation: it's very simple, and made only of primitive operations addition and squaring.

So, could a computer program recognize this theorem as surprising (or improbable)? Yes, but only if you give to the program a model where the coincidence between the two special cases occur.
A model could be of course a computer-vision software plus the ability to paint triangles and observe them, but could even be some much simpler linear algebra software.
The essential feature here is to recognize zero as a special case of real number and addition and squaring as special cases of mathematical functions.
And that is easily achievable if you have an axiomatization of real numbers and you measure the complexity of a number or function simply by using the length of their definition (taken as Shannon information measure)

In other words, both terms of the logical equivalence have a very small complexity (or information measure) if interpreted taking as model an axiomatization of real numbers.


==========================================================================

2. The Irrationality of the Square Root of 2

- Theorem expressed in a formal language: (Theorem number 1 from https://madiot.fr/coq100/)

Theorem sqrt2_not_rational : forall p q, q <> 0 -> p * p <> q * q * 2.


From a formal point of view, it says that a particular equation (p * p = q * q * 2) has no solution on the domain of natural numbers.

Should an equivalence of this kind be surprising? (or improbable)? The answer is NO: infact, most of diophantine equations have no solutions.

So, why do we find the theorem surprising?
Because square root of two is the measure of the square of side one, and every measure in the physical world is represented by a fraction (because measuring is a finite physical process: you can never find square root of two as a result of a measure in physics).

Then, if we give a computer a "physical" model of geometry (for example a world made of pixels), it could recognize, experimenting with it, that every length can be measured, and every measure is in fact a fraction. So, it could recognize as "surprising" (or statistically very improbable) a theorem that says that there is a measure that is not a fraction.

==========================================================================

3. Fundamental Theorem of Algebra

- Theorem expressed in a formal language: (Theorem number 2 from http://www.cse.unsw.edu.au/~kleing/top100/ - COQ version is very long if I include the necessary definitions)

lemma fundamental_theorem_of_algebra:
assumes nc: "¬ constant (poly p)"
shows "∃z::complex. poly p z = 0"


From a formal point of view, it says that every equation of a certain type (non constant polynomial) has always a solution on a certain domain (complex numbers).
Why should this be an exceptional case in comparison with a lot of other types of equations that always have solutions on certain domains?

First of all, a polynomial is a function that has a very simple definition (in the sense of low complexity): a polynomial is whatever function you can build using only "times" and "plus" operations with one variable. This fact alone makes it an interesting object.
A simple concept (as for complexity of it's definition) related to every function is it's inverse. So you easily discover that not all polynomials are invertible.
The surprising thing (that makes the theory more interesting), as we know, is the discovery of complex numbers: if you only take one polynomial that has no solution (the simplest one: "X * X = -1") and "pretend" that it had a solution by adding a new symbol "i" to the number system, then you discover that now all polynomials have a solution.
Complex numbers then become even more interesting when you discover that they correspond exactly to a SIMPLE geometric model (other coincidence).

Would a computer be able to "discover" complex numbers? I don't think so (at least not using the technologies currently used for artificial intelligence). But I think that a computer could be able to RECOGNIZE that complex numbers are an interesting concept by using a measure of how "improbable" are theorems when interpreted on the right models (meaning: the models that people have in mind when they say that they "understand" the theorem).

So, could a computer program recognize this theorem as surprising (or improbable)? — Mephist

You have (at least) two possible starting points. You can start from Euclid's classical axiomatic basis in geometry, or else axiomatize from number theory (Dedekind-Peano) by using a coordinate system. Euclid is much harder to reason from because it amounts to visual puzzling.

So, we can start from three two-tuples, say in a simple Cartesian coordinate system -- you can pick any coordinate system, really, and consider {(x1,y1),(x2,y2),(x3,y3)}. We can simplify by moving the triangle to the axes as following {(0,0),(0,yA),(xA,0)}. The angle in (0,0) is guaranteed to be perpendicular by the coordinate system itself. You can then trivially verify from the definition of distance=(x2-x1)²+(y2-y1)² that the distance between the two points that are not the origin. is xA²+yA². With every right-angled triangle isomorphic with the shape produced by picking a a point on each axis along with the origin, Pythagoras theorem easily follows from mere number theory. Instead of 2 points, you can pick 3,4, or more points, along with the origin and then derive other, similar distance invariants.

A model could be of course a computer-vision software plus the ability to paint triangles and observe them — Mephist

It is exactly this kind of visual puzzles that Immanuel Kant rejected in his Critique of Pure Reason. Classical Euclidean geometry is not pure reason, because it requires solving visual puzzles. Immanuel Kant was adamant: Pure reason is language only. It may only make use of symbol manipulation.

In other words, both terms of the logical equivalence have a very small complexity (or information measure) if interpreted taking as model an axiomatization of real numbers. — Mephist

Agreed. Pythogoras theorem is only surprising in a visual puzzling environment such as classical Greek geometry.

Then, if we give a computer a "physical" model of geometry (for example a world made of pixels), we could recognize, experimenting with it, that every length can be measured, and every measure is in fact a fraction. So, he could recognize as "surprising" (or statistically very improbable) a theorem that says that there is a measure that is not a fraction. — Mephist

Experimental testing is forbidden in math. Therefore, this approach by number sampling is very, very un-mathematical. In fact, you do not prove anything by sampling lots of numbers. The proof must be the result of judicious symbol manipulation instead.

and "pretend" that it had a solution by adding a new symbol "i" to the number system, then you discover that now all polynomials have a solution. — Mephist

For polynomials with coefficients in the rationals, you can indeed still reduce an otherwise irreducible polynomial by adding the appropriate field extension. Still, even adding i does not guarantee a closed-form solution for the roots (constructed using only supported field operators: + - * /), because we are not sure that there is a tower of radical field extensions available to achieve that. Even though adding i guarantees a solution, it may not spare you from having to approximate.

Would a computer be able to "discover" complex numbers? I don't think so — Mephist

Indeed, no. Gödel's incompleteness precludes that. It is generally not possible to discover new theorems by enumerating the domain of theorems and then verifying if they are provable in the theory.

But I think that a compute could be able to RECOGNIZE that complex numbers are an interesting concept by using a measure of how "improbable" are theorems when interpreted on the right models — Mephist

Well, you can solve a increasing number of polynomials with rational coefficients just by extending the rationals with judiciously chosen radicals. Therefore, it was probably not a far stretch to attempt to extend the rational calculation field with the positive solution of x²=-1 and give that symbol a name. In my impression, the surprising element is that you do not need to extend it further to guarantee a solution for all polynomials with rational coefficients, but not necessarily in closed form.

I think that the practice of using field extensions more or less guaranteed that i would be discovered ...

It is exactly this kind of visual puzzles that Immanuel Kant rejected in his Critique of Pure Reason. Classical Euclidean geometry is not pure reason, because it requires solving visual puzzles. Immanuel Kant was adamant: Pure reason is language only. It may only make use of symbol manipulation. — alcontali

Agreed. Pythogoras theorem is only surprising in a visual puzzling environment such as classical Greek geometry. — alcontali

Yes, and that's the point: you can't see the reason why Pythagoras theorem is interesting if you don't look at physical space. Then, we can say Pythagoras theorem is an interesting fact about physical space, and you can't "understand" it looking only at the logical (language only) formulation of the theorem, or even looking at it's proof. I guess a contemporary geometer would say that the exceptional fact is that the Riemann curvature tensor of physical space is zero (at least with a very good approximation).

You can of course restrict mathematical proofs to only make use of symbol manipulation. And that is the same thing as restricting proofs to use formal logic (more or less the standard of modern mathematics): a proof is a finite set of applications of a finite set of rules acting on a countable set of symbols.
But in my opinion even the use of "pure reason" relies ultimately on the ability to perform experiments in the physic world, only of a more "fundamental" level than the ones performed in euclidean geometry.
In fact, ultimately, a proof verification presupposes the existence of computable functions, and that presupposes the ability to perform a physical "experiment" that operates on a discrete set of distinguishable inputs and outputs, and is supposed to return always the same output when is given the same input. According to quantum mechanics, it's even not possible to build such an experiment with absolute certainty, since laws physics are not deterministic. So, I wouldn't attribute to "pure reason" a fundamentally non-physical character, as opposed to the physical character of Euclidean geometry.
In fact, Homotopy Type Theory has proved the equivalence between Homotopy Theory and Type Theory, and the existence of a model for both theories based on simplicial sets. So, HOTT formal logic corresponds to the use of topology on simplicial sets, that probably can be seen as the most fundamental laws of geometry.

Experimental testing is forbidden in math. Therefore, this approach by number sampling is very, very un-mathematical. In fact, you do not prove anything by sampling lots of numbers. The proof must be the result of judicious symbol manipulation instead. — alcontali

I am not saying that proving is based on number sampling. I am saying that understanding the meaning, or the importance of a theorem, is based on number sampling or, more generally, on performing experiments on (imaginary, and very often geometric) models. And that's exactly what is missing in a formal system such as Coq. What I am saying is that the expression of a theorem and it's proof in a formal logic system simply DOES NOT CONTAIN THE INFORMATION necessary to understand it, at least for a great part of the traditional "important" theorems (not all of them). And what mathematicians use in reality is information that is not contained in the formal (purely syntactical) expression of the theory, but is expressed in words and explanations written in plain english. So, a function (or an artificial intelligence system) capable to compute the "importance" of a theorem cannot be based on the logical formulation of the theory alone, but needs to take into account the model (often a physical model) on which the theory is interpreted.

There is an obvious reason why ancient Greek mathematicians regarded the irrationality of square root of two as a paradox: irrational numbers do not exist in nature! For them a length is a physical entity and a measure is a process made of splitting the segment in smaller and smaller parts until you find it's measure (expressed as a fraction). Infinite splitting is not a physical process. Then, irrational numbers cannot possibly exist as physical entity. This deduction is impossible to be made on the sole base of the formulation of the theorem "square root of two is irrational" (even by an human mathematician), simply because the information about the interpretation of fractions as physical measure is missing.

For polynomials with coefficients in the rationals, you can indeed still reduce an otherwise irreducible polynomial by adding the appropriate field extension. Still, even adding i does not guarantee a closed-form solution for the roots (constructed using only supported field operators: + - * /), because we are not sure that there is a tower of radical field extensions available to achieve that. Even though adding i guarantees a solution, it may not spare you from having to approximate. — alcontali

Yes, of course. I was considering a polynomial with coefficients in the real numbers. In this case the field extension obtained adding "i" corresponds to the field of complex numbers. I usually omit lots of details in my arguments, to make them shorter.

Indeed, no. Gödel's incompleteness precludes that. It is generally not possible to discover new theorems by enumerating the domain of theorems and then verifying if they are provable in the theory. — alcontali

I agree. I don't think this is due to Gödel's incompleteness. But I wasn't speaking about enumerating the domain of theorems. Actually, I wasn't even speaking about finding proofs automatically, but only defining a kind of "measure" of the relevance of a theorem based on the formulation of the theorem in a formal system AND it's interpretation on a model (that, in current mathematical practice, is usually not expressed in a formal language). The ability to recognize the relevance of theorems is obviously fundamental for a search strategy for theorems, but is in my opinion something completely different from enumerating proofs. It's somehow similar (but not the same thing) to searching the tree of positions in a chess game as opposed to evaluating a position: a function to evaluate positions is essential to a game strategy, but is not based on a blind simulation of the game. Understanding a theorem is not based on proof searching.

In my impression, the surprising element is that you do not need to extend it further to guarantee a solution for all polynomials with rational coefficients, but not necessarily in closed form. — alcontali

Yes, I agree. In fact, the theorem doesn't assert the existence of closed forms for solutions (obviously not true), but is based on the intuition that polynomial functions are continuous and surjective.

I think that the practice of using field extensions more or less guaranteed that i would be discovered ... — alcontali

Yes, but I would say that the algebraic concept of field extension is understandable once you have some concrete examples of field extension (as imaginary numbers). Algebraic concepts are usually generalizations of properties that several concrete modes have in common.

Just in general, there's a mathematical field (well, statistics) devoted to figuring out ways to take difficult qualitative concepts and develop quantitative indicators of their aspects. Operationalisation. Even if you can't boil the whole concept down to a number, sometimes you can boil some parts or simplifications of it down to a number, and it can be really surprising.

One good example is that if you want to measure the intensity of someone's experienced mental effort, you can measure their pupil dilation.

From a formal point of view, it's a logical equivalence between orthogonality of two vectors and an equation between real numbers (vectors' lengths).

Should an equivalence of this kind be surprising? (or improbable)? The answer is NO: in fact, whatever angle you take between two vectors, there will be an induced equation between vectors' lengths, and vice-versa. — Mephist

Hi Mephist,

I am very curious about this. Doesn't the vector's length follow from the Pythagorean theorem? If so, then it seems it isn't a simple logical equivalence, since the equation between real numbers (a vector's length) depends on the application of the theorem. Or is there an independent way of measuring a vector's length?


As to the OP: I sincerely believe that the importance of mathematical theorems really is a function of the aesthetic tastes of mathematicians which is partly based on certain objective factors: like whether the theorem unifies seemingly disparate areas of mathematics, whether the theorem has far-reaching implications within mathematics, etc. , as well as subjective factors: like how surprising it is, how difficult the theorem may have been to prove, how necessary it felt to the mathematician (i.e. the extent to which the mathematician feels like they discovered something), etc.

I am very curious about this. Doesn't the vector's length follow from the Pythagorean theorem? If so, then it seems it isn't a simple logical equivalence, since the equation between real numbers (a vector's length) depends on the application of the theorem. Or is there an independent way of measuring a vector's length? — Kornelius

Hi!

here's what I mean:
imagine you don't know anything about geometry: you are a computer without any way to "view" the world: no cameras, computer vision, or any kind of sensory system. Only a simple PC with a software to analyze theorems expressed in a formal logic.

You see this theorem:
forall A B C : PO, (orthogonal (vec A B) (vec A C)) <-> (Rsqr (distance B C) = Rsqr (distance A B) + Rsqr (distance A C)). [ I added parentheses to make it more readable: this is Pythagoras taken directly from here: https://madiot.fr/coq100/, no changes at all]

All you can see is this: IF you are given 3 objects of some type named PO (points), the theorem says that there is a "logical equivalence" ( the "if and only if" in the middle of the expression, written as "<->" ) between two propositions:
- proposition 1: "orthogonal (vec A B) (vec A C)"
- proposition 2: "Rsqr (distance B C) = Rsqr (distance A B) + Rsqr (distance A C)"

Now, you don't know what "orthogonal" and "vec" means. If you want, change the names into completely random strings. Could you guess that this is an interesting/important theorem?

All you know is that (vec A B) is an object, (vec A C) is another object, and "orthogonal" is a proposition speaking about these two objects.

Then we have the function Rsqr: you know what is Rsqr: it's the square root of a number: you are a calculator and you know how to compute the square root.
And then you have a function "distance" that takes two objects of type PO (points) and returns a number. You don't know how this function is implemented.

Given these conditions, this is not an "improbable" proposition because there are too many degrees of freedom: you can choose a random function for "distance" and on the base of that definition build the proposition "orthogonal" to make the equation become true.

But if you look at the model (interpretation) of the functions "orthogonal" and "distance" on the physical space, you discover that "orthogonal" is the only combination where the projection (the shade) of one vector over the other is exactly zero. And the function "distance" happens to be a very simple function of the length (it's square): so you have an improbable coincidence: a rare property of the angle coincides with a simple formula for the equation. If you define "orthogonal to be another angle, you can still define an equation that relates the lengths, but only making use of trigonometric equations (that are defined especially for this purpose; but Pythagoras' equation is one of the simplest expressions that you can build with addition and multiplication).
Ultimately, this depends on the fact that physical space is flat (zero curvature). If it was not flat the formula for the lengths of a straight triangle would have been a much more complex (random) equation.