Resolves YES iff the frontier research, new important scientific theorems are somehow formalized in a proof assistant (for instance Lean4).

For the purpose of this market I will consider this to be true if 90% most economically important theorems constructed in the year 2027 are formalized. A theorem is more economically valuable if it was paid for more either through salary or grant. I will figure out those theorems using the current state of the art LLM.

Example of some theorems not yet formalized: Noether's Theorem, Stone–von Neumann Theorem, Aharonov–Bohm Effect etc.

• Update 2025-05-23 (PST) (AI summary of creator comment): The creator has clarified the term "important for human civilization" (used to select theorems for the 90% formalization requirement):

  • It refers to theorems that are relevant for decision-making at that time (around the market's resolution period or 2030).

  • The emphasis is primarily on theorems that are economically useful, particularly for researchers in companies or similar applied settings.

• Update 2025-05-23 (PST) (AI summary of creator comment): The creator specifies that the set of 'most current important theorems' used for the 90% formalization target will be the top 100 most economically valuable theorems for each field (physics, mathematics, computer science).

• Update 2025-05-23 (PST) (AI summary of creator comment): The selection criteria for the 'most current important theorems' has been updated:

  • The set of theorems will be the most economically valuable theorems overall at the relevant time (around the market's resolution period or 2030).

  • This replaces the previous method of selecting the top 100 most economically valuable theorems from each individual field (physics, mathematics, computer science).

  • Consequently, the list of theorems will be a single, combined list, and the specific fields will no longer be used to create separate lists or apply quotas for theorem selection.

• Update 2025-05-23 (PST) (AI summary of creator comment): When determining the 'most economically valuable theorems':

  • The creator considers immediate pay (e.g., high salaries for relevant researchers, money paid for theorems) a significant indicator of economic value.

  • This is supported by the creator's view that immediate pay also reflects potential future economic value.

• Update 2025-05-23 (PST) (AI summary of creator comment): Regarding the use of immediate pay (e.g., salaries) to determine the economic value of theorems:

  • Pay attributed to teaching duties, as opposed to work directly on theorems, will be subtracted in the final estimation of economic value derived from an individual's salary.

• Update 2025-05-23 (PST) (AI summary of creator comment): The creator has clarified aspects of the theorems eligible for this market:

  • The market includes both scientific theorems and mathematical theorems.

  • Eligible theorems must be constructed from axiomatic principles specific to their field.