Is it possible to define a measure of how interesting is a given mathematical theory?

[mephist]

The measure should be a function that takes as input a library of propositions, definitions and proves in a given formal language (let's say for example a subset of mathlib - https://leanprover-community.github.io/ ... rview.html), and returns a real value between 0 and 1.

[alan1000]

The question is vague. What is meant by "interest"?

Of couse, all academics understand that at some periods of time, some issues are more fahionable than others. It is particularly important to remember this when you are looking for research funding! So that is one measure you could use. Or you could measure it by counting the number of articles, classified according to subject, submitted to journals. But any attempt at such a survey would be problematic. You could even try to measure it by the number of mentions in the popular press...

[Skepdick]

The measure should be a function that takes as input a library of propositions, definitions and proves in a given formal language (let's say for example a subset of mathlib - https://leanprover-community.github.io/ ... rview.html), and returns a real value between 0 and 1.

Sure, but your function is missing a depedency/input.

A full Mathematical description of the Mathematician relative to whom interest is being measured.

[Impenitent]

the third digit of pi (4) is shouted quite frequently on golf courses around the world...

does that mean it is interesting or just exclaimed loudly?

-Imp

[Sculptor]

The measure should be a function that takes as input a library of propositions, definitions and proves in a given formal language (let's say for example a subset of mathlib - https://leanprover-community.github.io/ ... rview.html), and returns a real value between 0 and 1.

Is it possible ?

No.

[Walker]

the third digit of pi (4) is shouted quite frequently on golf courses around the world...

does that mean it is interesting or just exclaimed loudly?

-Imp

It means, Incoming, tuck and duck! If panic ensues it also means lose balance and roll, which I saw happen once while on a green, to another putter while putting was in progress, likely because I put a bit too much urgency into the warning for customary dramatic effect as I watched the trajectory of another golfer's incoming approach shot and spontaneously calculated the end point.

https://www.youtube.com/watch?v=OophxEckcu0

[Impenitent]

the third digit of pi (4) is shouted quite frequently on golf courses around the world...

does that mean it is interesting or just exclaimed loudly?

-Imp

It means, Incoming, tuck and duck! If panic ensues it also means lose balance and roll, which I saw happen once while on a green, to another putter while putting was in progress, likely because I put a bit too much urgency into the warning for customary dramatic effect as I watched the trajectory of another golfer's incoming approach shot and spontaneously calculated the end point.

https://www.youtube.com/watch?v=OophxEckcu0

I liked the exploding gophers at the end of that movie

-Imp