Is this question about science or mathematical theorems?

@WilliamGunn Both. But they must be constructed from axiomatic principles in that field.

@patrik I'm afraid that's not how it works in biology. How does Lean4 handle a bunch of competing theories where one explains a little more of the variation than others, but nothing is really at the level of axiom?

@WilliamGunn In the description I said formalizable fields... But then removed it. Give me a second I'll bring it back.

@WilliamGunn Is it even a theorem if it's not based of axioms? I think in biology you have just guesses.

@patrik Appreciate it! Not all science is formalizable; in fact I think most isn't.

@patrik Call it what you want! This is actually a big theoretical vs experimental division. One is modeling the world based on observation and rarely has the luxury of proof, yet somehow is able to invest billions in multi-year research programs that are right enough to produce a return on investment and save millions of lives.

@WilliamGunn Of course. But fundamentally I'd say theorem by definition is formalizable. Regardless of the field.

@patrik I would have no problem with that. I asked because the question said "science discovery", but it's only a tiny fraction that's formalizable, so I wanted to understand whether you meant to include biology and psychology and sociology (to go down the "fields arranged by purity" axis) in frontier science discovery.

@WilliamGunn That makes a lot of sense. Will change the title.

If you were to resolve this today, what would the theorems be that you are calculating 90% of? There are some tricky judgment calls there, like:

- What does the "most current important theorems" mean? Does this include old theorems that remain important?
- What does "important for human civilisation" mean? Relevant right now or relevant on a long-time scale? I think almost no math research ranks very high on relevance for human civilisation, and very little physics/CS research will be high on relevance in the moment?

Or do you just want to delegate these judgments to the whims of the LLM?

@rayman2000 No I mean relevant for decisionmaking at that time. I specifically said in description "not historically".
I will write up the prompt that I will use to prompt the LLM about the theorems if this gets more bettors.
But it's mostly in the spirit of theorems that are economically useful for researchers in companies etc...

Let's say 90% of top 100 most economically valuable theorems for every field.

@patrik I think you will struggle to find even 10 "economically valuable" theorems from current mathematics research.
If I were setting up this question, I would probably use "submissions at the top journals/conferences".

@rayman2000 I don't want to do journals because they don't reflect as much what's actually being used. There are many theorems being used in AI research for instance and that is still technically mathematics. Maybe separating it by fields doesn't make that much sense in retrospect tho so let's make it 90% most economically valuable theorems at the given time overall.

@patrik I think the disconnect between academia and "real-world" research is a big problem in AI and a much smaller problem everywhere else. I would also disagree that "frontier research == currently economically valuable research", I think at least it should be "potential future economic value", which is of course hard to measure, but that's why it's frontier research?
And then will you define a cut-off date for how recent the theorems have to be? Otherwise, we have to argue about what the economic value of the fundamental theorem of calculus is.

@rayman2000 What about this: "Theorems constructed in the year 2027 sorted in the order of how much money was paid for them" So AI researchers formalizing things would be high because they have high salaries and that can be considered pay for those theorems.

And immediate pay also reflects potential future economic value.

@patrik Hmm, but professors are mostly paid pretty well, I feel that will not work well with your desire to go for things which "are actually used"
(also thank you for indulging my nitpicky discussion on resolution criteria, I think it will be pretty clear whether everything is formalised or not, I just enjoy picking at unclear criteria 😃 )

@rayman2000 That's fine with me. Also if most of the pay is because of the teaching not theorems that would be subtracted in the final estimation.

@rayman2000 You nitpicking makes this market better 👍

@patrik OK it looks well-defined to me now! Have fun actually calculating it though 😛