The Math Genome Project

Stream: general

[John Mercer]

Hi fellow Lean lovers,

Excited to inform you about the launch of The Math Genome Project! It’s a new platform designed to bring formal math mainstream, and you can sign up for the waitlist here (batches are added monthly):

https://www.themathgenome.com/

The platform offers a range of features such as the largest integrated (formal and informal) theorem database in the world, real-time multi-user theorem proving collaboration in a gamified and optional no-code experience, and marketplace features such as bounties. With these features, formal theorem provers can collaborate with others and make money by writing proofs and teaching theorem proving, all within your browser.

Why is it called “The Math Genome Project”?

The Human Genome Project (1990-2003) was an international collaboration to create a standard and reliable map of the human genome, and became the foundation and catalyst of 21st century discoveries, therapies and preventions of human disease.

In this same spirit and recognition of the need for a unified large-scale approach, The Math Genome Project is standing on the shoulders of the brilliant and passionate mathematicians and computer scientists that have spent decades of grass-roots formalization efforts (such as Coq, Isabelle/HOL, Mizar, Lean, Metamath) to unify, organize, and empower these communities to bring the joy of formal mathematics mainstream.

Built on a modern technology platform for the creation, standardization, synthesis and verification of formal systems, we're doing this by providing a marketplace for creating, learning, teaching and collaboration that enables formal math lovers to monetize their skills and experience and ultimately spend more time doing what they love. What was once a hobby or passion project can become a career or serious side-hustle for lovers of mathematical knowledge. What was once only known to professional mathematicians (or a few experts in an esoteric field), will be accessible and more easily learned by anyone.

Whereas the Human Genome Project was a terminal project with fixed endpoint, the goal of the Math Genome Project is to become the technology platform that underpins and enables humanity to reach the full potential of formalized mathematics (and physics!) indefinitely and become the standard and reliable map of all known mathematics - a modern platform to realize the vision of the QED Manifesto.

What do we do from here?

1. Please sign up for the waitlist! (this will also help close our VC funding round faster)

2. Please provide your feedback and thoughts in this channel

3. Please spread the word! Our social accounts are on website :)

4. Would love to form a Lean Advisory Board to help with strategy and product roadmap (e.g. dependencies, features and synthesizing community feedback for prioritization).

So excited to build the future of math together!

[Julian Berman]

I have quite superficial first-impression feedback, which I almost hesitate therefore to offer, but in the hopes it's constructive, particularly given it's literally a first impression because it's the first thing one reads on the site -- I think your teaser is not going to do the site/platform favors. Specifically "Make money while building your brand and following doing formal proofs." to me reads somewhere between over-the-top at best and fishy at worst -- even seeing all the wonderful things this community does (and I'm sure the wider formal proof community is similar).

[Julian Berman]

Specifically I would definitely deemphasize the "building your brand" bits which appear both there and I see elsewhere in the description, and definitely focus slightly more on the details of what the thing actually is -- I assume the goal is to help people navigate where formal proofs live somehow, and potentially more than just where.

But saying "build your brand", "gamified experience" and "equal opportunity" in the first paragraph is I think going to land very flat with the target audience for this sort of thing

[Jason Rute]

Here is a clickable link: https://www.themathgenome.com/

[Jason Rute]

(Was hard in the mobile app to use your link.)

[Julian Berman]

(moved)

[Scott Morrison]

Yes, I'm not even bothering to click through based on the bad taste that description left.

[John Mercer]

Julian Berman said:

I have quite superficial first-impression feedback, which I almost hesitate therefore to offer, but in the hopes it's constructive, particularly given it's literally a first impression because it's the first thing one reads on the site -- I think your teaser is not going to do the site/platform favors. Specifically "Make money while building your brand and following doing formal proofs." to me reads somewhere between over-the-top at best and fishy at worst -- even seeing all the wonderful things this community does (and I'm sure the wider formal proof community is similar).

Thanks so much for the great feedback!! This is exactly the kind of helpful feedback needed (and you were very kind about it too lol!). Will change it immediately, but will explain the "why" behind it: I've been in these communities for years and see how passionate people are about formal math, and yet, it's often the case it's "on the side" from their professional work. This platform can people make formal math full-time and so wanted to put the economics front-and-center.

Thanks again for your patience and so helpful feedback @Julian Berman !

[John Mercer]

Jason Rute said:

Here is a clickable link: https://www.themathgenome.com/

Oh thanks @Jason Rute , updated the link to make it clickable (doh!)

[John Mercer]

Scott Morrison said:

Yes, I'm not even bothering to click through based on the bad taste that description left.

@Oisin McGuinness @Scott Morrison , first iteration update is live if you refresh. Hope you'll forgive and give it another chance :)

It's now "A collaboration platform and marketplace for the formalization of mathematics and theorem proving."

Had ^^ there originally but thought it was too wordy :man_shrugging:

[Eric Wieser]

More proofs, less tears and equal opportunity for all.

An oxford comma here would save you from promoting "less equal opportunity for all" :upside_down:

[Jason Rute]

@John Mercer The issue is less about wordiness, but more about substance vs hype. It isn't clear you have a vision that really aligns with what people are asking for. Your image on your website does show a lot of the big needs in interactive theorem proving such as better usability of systems, more powerful AI/ATP tools, and better interconnectivity of ITP systems. But at the same time, it isn't clear you are offering any real solutions of substance. And it also isn't clear how you plan to monetize this (and even the clear single that you do plan to quickly monetize this is off-putting to this community). Add on top of that, you are making claims which sound too good to be true like the "largest integrated (formal and informal) theorem database in the world" and a "no code experience". :rolling_eyes:

[Jason Rute]

(I crossed out the stuff about monetization since I think it is beside the point.)

[Julian Berman]

Yeah. The target audience (someone who even cares or knows what "formal proof" or heck "mathematics" means) is too savvy for the level of marketing hype you're projecting.

(I was going to say something specifically about the database bit too -- I was/am presuming you're going to essentially be extracting proofs from lots of places' GitHub repos like mathlib -- so I'd hesitate to say you're a bigger database than the place you pulled the proofs from even :) -- but this is the sort of hype-y thing that sometimes is good but in very very small bits and when there's clear substance to back it up -- meaning where someone is so impressed by other stuff that they're willing to suspend belief for extra over-the-top-ness.)

[Junyan Xu]

This thread from last year may be relevant, FWIW.

I guess something like the incredible proof machine could be considered no-code :) Terry Tao also made something in 2018-19. LLM autoformalization is definitely a new possibility :)

[John Mercer]

Junyan Xu said:

This thread from last year may be relevant, FWIW.

I guess something like the incredible proof machine could be considered no-code :) Terry Tao also made something in 2018-19. LLM autoformalization is definitely a new possibility :)

Thanks Junyan! btw, your github handle is hilarious!! :joy:

[John Mercer]

Julian Berman said:

Yeah. The target audience (someone who even cares or knows what "formal proof" or heck "mathematics" means) is too savvy for the level of marketing hype you're projecting.

(I was going to say something specifically about the database bit too -- I was/am presuming you're going to essentially be extracting proofs from lots of places' GitHub repos like mathlib -- so I'd hesitate to say you're a bigger database than the place you pulled the proofs from even :) -- but this is the sort of hype-y thing that sometimes is good but in very very small bits and when there's clear substance to back it up -- meaning where someone is so impressed by other stuff that they're willing to suspend belief for extra over-the-top-ness.)

@Jason Rute and @Julian Berman Thanks so much for the feedback - I get it guys! There’s a few things going on here so let me unpack them briefly (ultimately the proof is in the pudding, so would rather be workin to get batches in vs. trying to write about it):

1. There are several segments I have to solve for in the early days of the landing page: formal math lovers yes - but also investors, the other 95% of math community, students/gamers to help them see the future of math. It’s tricky and appreciate everyones patience until converge to optimal messaging.

2. I appreciate the skepticism (and expect nothing less from this community! :)) and look forward to removing the “waitlist.” The MVP is almost ready and still working on the bounty system and no-code feature set (inspired by Scratch developed at MIT).

3. Regarding the database claim, the key word is “integrated” - there is no other place (to my knowledge) to access both informal (in LaTeX) and formal proofs. Yes, various sources are being harvested (still automating it so continuous) but the goal is realize the vision of the QED manifesto and have all math in one place in a way that is harmonized and standardized so it’s computable (source eg’s include Wikipedia, proofWiki, Math arXiv, etc). One future note, a strategic goal is to get partnerships with journals to get access to only theorems/proofs for harvesting that will link back to the rest of the journal article (i.e., even if the whole thing it behind a paywall, can we at least get access to some of it?!).

[Yaël Dillies]

I can't help but say that given your background there are more impactful and direct things that you can achieve for us. Typically, a command line-less install of Lean+mathlib keeps coming up. Eg https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20Microsoft.20made.20Windows

[John Mercer]

Yaël Dillies said:

I can't help but say that given your background there are more impactful and direct things that you can achieve for us. Typically, a command line-less install of Lean+mathlib keeps coming up. Eg https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20Microsoft.20made.20Windows

Thank you for the feedback @Yaël Dillies! A pillar of our phase I strategy and roadmap is "Remove barriers-to-entry for new users" so this is additional validation our strategy is correct! After the early releases, we will provide several mechanisms for the respective communities to help us with the roadmap (prioritization and specifications). Have a look at Careers > Ambassador Program, these ambassadors will also have access to our Jira as we scope and prioritize epics/features.

[Notification Bot]

Chris Hughes has marked this topic as resolved.

[Notification Bot]

Chris Hughes has marked this topic as unresolved.

[Jireh Loreaux]

@John Mercer this is not intended as argumentative, it's an honest question: why would someone who is interested in Lean and developing a library of formal mathematics apply to work at The Math Genome as opposed to simply contributing to mathlib (or related Lean projects)? For example, I don't entirely understand the revenue stream for The Math Genome, and it's also not clear what licenses will be attached to your employees' work. Do you acquire the IP, or is it publicly available?

[John Mercer]

Jireh Loreaux said:

John Mercer this is not intended as argumentative, it's an honest question: why would someone who is interested in Lean and developing a library of formal mathematics apply to work at The Math Genome as opposed to simply contributing to mathlib (or related Lean projects)? For example, I don't entirely understand the revenue stream for The Math Genome, and it's also not clear what licenses will be attached to your employees' work. Do you acquire the IP, or is it publicly available?

Hi @Jireh Loreaux , thanks for the question, it's a great one and makes me think I should have added a Q&A to demystify some things.

1. As a mathematician at TMGP, you get to work at the intersection of formal math and product development. A good analogy is industry product data science teams working with product/engineering to build data and ML/AI driven user experiences in a SaaS platform.
2. All formal and informal math will be available at free tier (i.e., public). The business model is SaaS + marketplace commission model + API. We're going to connect the >95% of math done informally with formalization experts that can write formal proofs and receive the proof bounties (as a marketplace, we'd get a small % like a PayPal transaction fee). But anyone can contribute to a bounty for proofs they'd love to see formalized. SaaS is for additional Pro features, product experiences and for classroom licensing/features. Standard API (per token or call) for using the enriched data layer for 3rd party work (e.g. a lot of people in many of the communities want to work on ATP, but there is data engineering barriers to entry).
3. TMGP won't supplant open-source community work, quite the opposite - complement and accelerate it... it's a conduit to extend your impact! :heart: :rocket:

[Chris Hughes]

John Mercer said:

2. All formal and informal math will be available at free tier (i.e., public). The business model is SaaS + marketplace commission model + API. We're going to connect the >95% of math done informally with formalization experts that can write formal proofs and receive the proof bounties (as a marketplace, we'd get a small % like a PayPal transaction fee). But anyone can contribute to a bounty for proofs they'd love to see formalized. SaaS is for additional Pro features, product experiences and for classroom licensing/features. Standard API (per token or call) for using the enriched data layer for 3rd party work (e.g. a lot of people in many of the communities want to work on ATP, but there is data engineering barriers to entry).

My main concern with this bounty system is that a project like mathlib is very much a collaborative project and it is often not clear who to give credit to for a proof. Whenever people set out to prove some large famous theorem there is usually a large amount of unglamorous background theory and refactoring of various concepts in mathlib that have to be done first. In the paper about Dedekind Domains by Sander R. Dahmen, Ashvni Narayanan and Filippo A. E. Nuccio Mortarino Majno di Capriglio, they emphasise "Due to the decentralized organization and fluid nature of contributions to mathlib, its contents are built up of many different contributions from over 250 different authors. Attributing each formalization to a single set of main authors would not do justice to all others whose additions and tweaks are essential to its current use." Formalized maths is more about theories and a unified library than it is about famous theorems.

This depends a little on the type of theorems you anticipate bounties being offered for. I think the system might work okay for certain kinds of proof, but probably not something like the Liquid Tensor Experiment for example.

[John Mercer]

Chris Hughes said:

John Mercer said:

2. All formal and informal math will be available at free tier (i.e., public). The business model is SaaS + marketplace commission model + API. We're going to connect the >95% of math done informally with formalization experts that can write formal proofs and receive the proof bounties (as a marketplace, we'd get a small % like a PayPal transaction fee). But anyone can contribute to a bounty for proofs they'd love to see formalized. SaaS is for additional Pro features, product experiences and for classroom licensing/features. Standard API (per token or call) for using the enriched data layer for 3rd party work (e.g. a lot of people in many of the communities want to work on ATP, but there is data engineering barriers to entry).

My main concern with this bounty system is that a project like mathlib is very much a collaborative project and it is often not clear who to give credit to for a proof. Whenever people set out to prove some large famous theorem there is usually a large amount of unglamorous background theory and refactoring of various concepts in mathlib that have to be done first. In the paper about Dedekind Domains by Sander R. Dahmen, Ashvni Narayanan and Filippo A. E. Nuccio Mortarino Majno di Capriglio, they emphasise "Due to the decentralized organization and fluid nature of contributions to mathlib, its contents are built up of many different contributions from over 250 different authors. Attributing each formalization to a single set of main authors would not do justice to all others whose additions and tweaks are essential to its current use." Formalized maths is more about theories and a unified library than it is about famous theorems.

This depends a little on the type of theorems you anticipate bounties being offered for. I think the system might work okay for certain kinds of proof, but probably not something like the Liquid Tensor Experiment for example.

Thanks so much for the comment @Chris Hughes ! Exactly the discussion needed when building out people>1 bounty functionality! So in the case of n>1 (let's take your extreme example), would a community allocation decision be sufficient? Here's how it would look like and consistent with current development: 1. the stacked avatars of everyone working on the bounty are shown for all proofs under dev; 2. if :octopus: , then it goes to "team allocation step" where those on the list would collectively assign a % of the bounty to the members on the list; 3. Each member of the list must "accept distribution" and once all team members accept, the transaction continues and funds are distributed.

Does that "extra step" in the process for people>1 sound good? (in the case of people=1, once it's verified, it immediately calls the release funds api). I suspect big contributions like LTE, the community can assign a smaller group of representatives to decide and make the allocation decision for the rest of the group, so that not everyone has to accept individually for the funds to be distributed.

[Jireh Loreaux]

First, that proposal is susceptible to permanently avoiding payout if one contributor opts never to accept the distribution.

Second, I think it's much less obvious than it seems. For instance, let's say someone is working on a bounty and someone else develops a tactic for mathlib in general, but it just so happens to be extremely useful for working on the problem with the bounty. How does that person get credit or remuneration? I think this, along with other general background theory, is more along the lines of what Chris had in mind. The point is that it's difficult to disentangle the work done on a bounty from the general public service of contributing to something like mathlib. Where are the lines drawn?

[Yaël Dillies]

And what to do about general library maintenance? I mostly do this at this point, and it's not clear how I contribute to any particular big result, even though I probably made someone's life slightly less miserable at some point.

[Yaël Dillies]

(You could reply that we should hire me as a full-time maintainer, and I wouldn't disagree! but, again, where would the money come from?)

[Chris Hughes]

There's also the problem of encouraging a "race to the finish" approach that doesn't actually produce a usable theorem, or prove the prerequisites in a way that's useful to other people. There's a bit of a mantra in the community now that if it's not in mathlib it doesn't count. Proofs break and even theorem statements change, so proofs are only really usable if they've been contributed to mathlib.

[John Mercer]

Jireh Loreaux said:

I hear you @Jireh Loreaux here some quick points:

First, that proposal is susceptible to permanently avoiding payout if one contributor opts never to accept the distribution.

yes, I know. However, if the community is fair and thoughtful then should minimize risk and we could add rules that x% have to accept to push the transaction. Product dev is an iterative process and we have to think about broad strokes and "is it directionally better" - doesn't get solved the first go most of the time.

Second, I think it's much less obvious than it seems. For instance, let's say someone is working on a bounty and someone else develops a tactic for mathlib in general, but it just so happens to be extremely useful for working on the problem with the bounty. How does that person get credit or remuneration? I think this, along with other general background theory, is more along the lines of what Chris had in mind. The point is that it's difficult to disentangle the work done on a bounty from the general public service of contributing to something like mathlib. Where are the lines drawn?

I understand re: the value of theory dev and maintenance. As an example, we can bake that into the commission %, and these are the types of responsibilities of the staff mathematicians that continue to work on mathlib would have. For those that contribute to mathlib but aren't full-time employees, we could add % points to then allocate to independent contributors (again, ideation and we'll converge to what's best)

But let's not miss the point: All these are solvable through iteration/refinement :)

[John Mercer]

Yaël Dillies said:

(You could reply that we should hire me as a full-time maintainer, and I wouldn't disagree! but, again, where would the money come from?)

Absolutely @Yaël Dillies , it's a founding motivation to create the marketplace that enables formal mathematicians to replace their day job with their night job, i.e. do this as a full-time job and have a career path :smiling_face_with_hearts:

[Damiano Testa]

I think that most of the projects that end up in mathlib should probably end up funding mathlib itself. This seems fairer than disentangling individual contributions and percentages.

[John Mercer]

Personal goal: get my first :thumbs_up:. It's going to be :joy: ... like, tell-my-kids-at-dinner level :joy:!

[Damiano Testa]

It's a tough crowd...

[Julian Berman]

I'll just throw in that the open source software community, or platforms servicing it, has struggled with this very similar question the past few years and has essentially thrown its hands up and called it too complex to have a general solution. TideLift and Thanks.dev (which are the two I interact with) funnel funds from people who rely on projects to people who contribute to those projects, but they do not help (nor plan to AFAIK) with the project deciding how to allocate funds to its contributors, because it's often impossible to figure out for the reasons above -- unclear what the right allocation is, projects are more than just lines of code contributed, etc.

[Arthur Paulino]

John Mercer said:

Personal goal: get my first :thumbs_up:. It's going to be :joy: ... like, tell-my-kids-at-dinner level :joy:!

Let me try to help you. I think your business plan lacks clarity. You'd need to be more precise about the flow of money and how it relates to the dynamics of the math library you're aiming to develop.

Formalizing mathematics is a tough task. It's not just about getting theorems to typecheck... but also about getting definitions right. And let's not forget the effort that needs to be put on the infra to keep the train going.

There seems to be little concern about the fact that a big chunk of this community is focusing on developing mathlib (a Lean lib), and that asking people to start developing something else is a big ask. How do you want to convince these people that your infra will be more fruitful than mathlib's to the point of changing their minds?

[PCloud]

If you just want to add a bounty program to mathlib, that is a solved problem - just put your money on Bountysource.
But you need to understand that the main reason why theorems don't get formalized is not because there is no money attach to it...

[Mauricio Collares]

To be fair, the way mathlib currently works is that "architects" (people who know the subject material enough to break it into a detailed blueprint) are also the people who do the gruntwork of proving the small "math-obvious" lemmas. This works, but math is one of those few cases where leaving the small details to less experienced contributors (a la big-design-up-front/waterfall style development), who might be interested in getting paid for it, can also work.

[Eric Wieser]

I don't see it mentioned above, so I'll remark that I find the "harmonized and standardized" (across other proof assistants) claim hard to believe. As far as I'm aware, this is an open area of research, fraught with difficulties such as:

• Types of objects in the library of one language being fundamentally unrepresentable in another language
• Users not wanting to have to translate betweenNat vs FromCoq.Nat vs FromIsabelle.Nat; a key feature of mathlib is that it strives to have a canonical way to spell things. Even on the possibly-generous assumption that other libraries do the same, this still leaves you with a choice of 5 ways to spell things, one for each system. It's highly likely that some of these will have mathematically different meanings in different systems.
• Pretending two types from different systems are equivalent without proof amounts to unsoundness

[Chris Hughes]

PCloud said:

If you just want to add a bounty program to mathlib, that is a solved problem - just put your money on Bountysource.
But you need to understand that the main reason why theorems don't get formalized is not because there is no money attach to it...

Money is absolutely a reason I don't work too much on mathlib any more.

[Eric Wieser]

My experience with bounty programs is that the amounts can be life-changing (both financially and legally...) for those living in developing countries, but are often inadequate to support a developer living in a high COL area. This is great for attracting new and diverse talent, but doesn't necessarily help much with supporting people like Chris.

[Giovanni Mascellani]

Eric Wieser said:

My experience with bounty programs is that the amounts can be life-changing (both financially and legally...) for those living in developing countries, but are often inadequate to support a developer living in a high COL area. This is great for attracting new and diverse talent, but doesn't necessarily help much with supporting people like Chris.

That depends a lot on how much money it is. I wouldn't say I live in a really high COL area, but not even in a developing country. My current day job pays me (and many other people) a good salary for contributing daily to a free software project I already contributed to in my spare time before having this job. Of course my contribution amount increased by orders of magnitude. If somebody with enough entrepreneurial ability manages to find ways to fund free software projects, in general I think that's a good thing. Of course it can also have risks, so it's good to be careful.

This reminds me of a recently published report about money usage in Debian, investigating in particular how the community would react to the hypothesis of paying contributors: https://lists.debian.org/debian-devel-announce/2023/04/msg00001.html. It doesn't necessarily translate 1:1 to mathlib, but maybe it's an interesting read.

[John Mercer]

This is such a wonderful conversation trajectory! Just posting to let you know I'll respond to all sometime this evening and also summarize the feedback for the week to make sure I understand/address everything. :thank_you:

[Tyler Josephson ⚛️]

As a Lean enthusiast who is not a mathematician (chemical engineer/computational chemist), I have a few thoughts:

1) I wonder who the “customers” would be (those willing to pay). Perhaps these could be scientists/engineers (or their employers) who value formal methods, but personally lack the experience to write proofs. The only way they can get help now is from volunteers in the Lean community. I haven’t felt that volunteers are inadequate, since the current Lean-for-science community is small.

[Tyler Josephson ⚛️]

2) The math folks here resist the hype; they have a good idea of what they want/need, after all. For those outside formal methods, I think “selling” the idea needs to happen, otherwise they won’t care (but you still need to ground the pitch in substance, not hype). I’ve spent a lot of time thinking, writing, and explaining “what can Lean do for you” - the promise of bug-free code is likely the idea that gets the most traction.

[Tyler Josephson ⚛️]

3) I wonder if the task “rewrite this Python code in Lean 4, and write and prove some theorems that the math is correct” is something monetizable. Right now, my research group is paying several grad and undergrad researchers to work full time on things that are basically like this. We’re more concerned about teaching and learning than we are about “getting the code written” (we are, after all, paying PhD stipends), but if demand from scientists / engineers were to scale, there might be others willing to pay a bounty to “get the code from whoever.”

[Tyler Josephson ⚛️]

4) Having informal proofs in natural language / LaTeX, and pairing these with corresponding formal proofs/code, will be the key to communicating with this population. The math jargon in mathlib is a barrier to those with essentially a sophomore’s math training. I like the places in mathlib where proofs and definitions are described with LaTeX. For explaining mathlib in natural language on a large scale or on an individualized basis, I’m hoping for LLM tools to do informal-formal machine translation / autoformalization. There’s still a lot of work to be done on that; maybe OpenAI could be a client that pays people to write training data with informal/formal pairs.

[John Mercer]

Arthur Paulino said:

John Mercer said:

Personal goal: get my first :thumbs_up:. It's going to be :joy: ... like, tell-my-kids-at-dinner level :joy:!

Let me try to help you. I think your business plan lacks clarity. You'd need to be more precise about the flow of money and how it relates to the dynamics of the math library you're aiming to develop.

Formalizing mathematics is a tough task. It's not just about getting theorems to typecheck... but also about getting definitions right. And let's not forget the effort that needs to be put on the infra to keep the train going.

There seems to be little concern about the fact that a big chunk of this community is focusing on developing mathlib (a Lean lib), and that asking people to start developing something else is a big ask. How do you want to convince these people that your infra will be more fruitful than mathlib's to the point of changing their minds?

This is really helpful @Arthur Paulino and really crystallizes the umbrella topic of the relationship between mathlib repo and TMGP platform. (as @Chris Hughes echoed the matra, if not in mathlib then doesn't count.) I think about -probably too simply- as things that can be done by using mathlib and those that require adding/mutating. To chip away at the problem and meet the goals of this phase, my current thinking is to avoid this deeper integration problem initially so it's read-only, so to speak, with the current state of mathlib (in the respective session) and that focuses the MVP to on an easier Lean learning experience (with all the other bells/whistles of having informal proofs and no-code/chat/gamification). This would then position us to assess/design the if/how/when for a deeper integration.

[John Mercer]

PCloud said:

If you just want to add a bounty program to mathlib, that is a solved problem - just put your money on Bountysource.
But you need to understand that the main reason why theorems don't get formalized is not because there is no money attach to it...

Thanks for this comment @PCloud , it really further motivated the discussion and the great feedback/validation from @Chris Hughes

[John Mercer]

Eric Wieser said:

I don't see it mentioned above, so I'll remark that I find the "harmonized and standardized" (across other proof assistants) claim hard to believe. As far as I'm aware, this is an open area of research, fraught with difficulties such as:

• Types of objects in the library of one language being fundamentally unrepresentable in another language
• Users not wanting to have to translate betweenNat vs FromCoq.Nat vs FromIsabelle.Nat; a key feature of mathlib is that it strives to have a canonical way to spell things. Even on the possibly-generous assumption that other libraries do the same, this still leaves you with a choice of 5 ways to spell things, one for each system. It's highly likely that some of these will have mathematically different meanings in different systems.
• Pretending two types from different systems are equivalent without proof amounts to unsoundness

Hi @Eric Wieser , again, I should have elaborated and had FAQ. "harmonized and standardized" is not so much a deeper category theory of languages but rather simpler experiences like searching and comparing. With fragmented/siloed communities and locations of dbs and metadata (in different formats/structures), it's not possible to have the product experiences we expect elsewhere in our professional/personal lives. Let me take a simple yet powerful and shocking example: how many informal claims/proofs exist? What are their names and statements and what field? This list doesn't exist, but is part of TMGP database. And which of those map to theory in respective formal systems? (beyond 100 theorems list! :)) "harmonized and standardized" also enables us to join those informal statements to theory/implementations across systems for other types of queries. My design philosophy of data and compute ecosystems is that they should become a big lego box that you can build anything from (downstream data assets, methods/models and product experiences). You can't do that without the system design and data eng dirty work under the mission of a single unified data ecosystem for informal/formal math. Also note, not trying to unify the dev of languages into one-to-rule-them-all, but rather, enable each of them to reach more people. And to take your specific example, this is an example of enrichment where we can enrich after ingestion to provide those mapping tables that enable people to at least compare implementations in a standard way (vs having multiple doc tabs and env's open for different systems).

[John Mercer]

Chris Hughes said:

PCloud said:

If you just want to add a bounty program to mathlib, that is a solved problem - just put your money on Bountysource.
But you need to understand that the main reason why theorems don't get formalized is not because there is no money attach to it...

Money is absolutely a reason I don't work too much on mathlib any more.

Thank you for sharing this @Chris Hughes, might not have intended it but personally it meant a lot to me. This is exactly the reality that TMGP is trying to change in the future. I've been a bit of a "silent & observing product manager" in these communities for some time, and a founding market assumption is that there is a huge void for a marketplace for people that feel just like you (and me) that would rather being doing formal math full-time but are beholden to their day jobs.

[John Mercer]

Eric Wieser said:

My experience with bounty programs is that the amounts can be life-changing (both financially and legally...) for those living in developing countries, but are often inadequate to support a developer living in a high COL area. This is great for attracting new and diverse talent, but doesn't necessarily help much with supporting people like Chris.

Let's change some lives @Eric Wieser!! - for Chris and lot more people... I have this recurring vision of some kid on a OLPC in their browser formalizing a little lemma for someone's paper, getting a bounty and being added as coauthor. :heart_eyes:

[John Mercer]

Tyler Josephson ⚛️ said:

As a Lean enthusiast who is not a mathematician (chemical engineer/computational chemist), I have a few thoughts:

1) I wonder who the “customers” would be (those willing to pay). Perhaps these could be scientists/engineers (or their employers) who value formal methods, but personally lack the experience to write proofs. The only way they can get help now is from volunteers in the Lean community. I haven’t felt that volunteers are inadequate, since the current Lean-for-science community is small.

Awesome thanks @Tyler Josephson ⚛️ , this is exactly what the marketplace is- connecting informal claims to formal provers. I've done the research on the enterprise side of formal languages for high-risk systems (like Dafny for program verification) but the goal in the first year was really focused on extending formal math to more of the math community (so that papers published include formal proofs (think PapersWithCode) and more students learn formal math in their math programs).

[David Loeffler]

John Mercer said:

Eric Wieser said:

I don't see it mentioned above, so I'll remark that I find the "harmonized and standardized" (across other proof assistants) claim hard to believe. As far as I'm aware, this is an open area of research, fraught with difficulties such as: [...]

Hi Eric Wieser , again, I should have elaborated and had FAQ. [...]

@John Mercer I think you need to try doing less talking, and more listening.

In this thread, least half a dozen people – all of whom are hugely experienced practitioners of formal mathematics – have raised specific queries and critiques of your proposal, and I don't see any sign that you have actually engaged with any of them. You haven't made any coherent response to Eric's point, about it being difficult to connect together formal proofs in multiple languages in a logically sound way; you claim you've already anticipated the issue, but I don't think you've even understood the issue at all – you've just tried to bury it in a flood of verbiage.

Every new claim you've made seems less plausible than the last. E.g. you're now claiming that you're going to build a complete database of every mathematical theorem ever written. Do you have any idea how large a dataset that is, and how messy? You're glossing over problems which huge teams of very smart people have spent years trying to solve, seemingly believing that you can solve them with nothing more than marketing buzzwords.

[Mario Carneiro]

I was going to say the exact opposite, I am glad John Mercer is actually thoughtfully communicating on this sensitive topic and trying to respond to criticism. I have seen other projects in this general direction before but I think they are handling it well.

[Mario Carneiro]

Every new claim you've made seems less plausible than the last. E.g. you're now claiming that you're going to build a complete database of every mathematical theorem ever written. Do you have any idea how large a dataset that is, and how messy?

If you lower your standards to what amounts to a google search, it is not that unreasonable to have something close to a database of every theorem that has been digitized in some way.

[Mario Carneiro]

Plus, aspirational goals are allowed to be superlative. The point is to point the project in the right direction, not to be a deliverable with a due date

[Tyler Josephson ⚛️]

I am reminded of Wolfram’s database of >300k formulae. Not formalized and not about proofs, but impressive nonetheless.

[Eric Wieser]

David Loeffler said:

You haven't made any coherent response to Eric's point, about it being difficult to connect together formal proofs in multiple languages in a logically sound way;

My reading of @John Mercer's answer is that there's a lot of value to connecting together formal proofs even if it's only in an informal way; indeed, if a collaborator wanted to use Coq instead of lean, a large database that helped me find analogous lemmas to the ones I've memorized in lean would certainly prove useful

[John Mercer]

Mario Carneiro said:

Every new claim you've made seems less plausible than the last. E.g. you're now claiming that you're going to build a complete database of every mathematical theorem ever written. Do you have any idea how large a dataset that is, and how messy?

If you lower your standards to what amounts to a google search, it is not that unreasonable to have something close to a database of every theorem that has been digitized in some way.

Thanks @Mario Carneiro, that's a great way to put it (screenshot below):
image.png

[John Mercer]

Eric Wieser said:

David Loeffler said:

You haven't made any coherent response to Eric's point, about it being difficult to connect together formal proofs in multiple languages in a logically sound way;

My reading of John Mercer's answer is that there's a lot of value to connecting together formal proofs even if it's only in an informal way; indeed, if a collaborator wanted to use Coq instead of lean, a large database that helped me find analogous lemmas to the ones I've memorized in lean would certainly prove useful

Thanks @Eric Wieser , yep informal is defined as side-by-side right now (see below), and in future we can enhance the comparative analysis.
image.png

[John Mercer]

Tyler Josephson ⚛️ said:

I am reminded of Wolfram’s database of >300k formulae. Not formalized and not about proofs, but impressive nonetheless.

Related note, I'll be working with Stephen on some aspect (still converging) of the TMGP at his summer school.

[Eric Wieser]

Your website would be a lot more convincing with some screenshots like these!

[Eric Wieser]

(I'm sure you're aware, but it looks like your syntax highlighter isn't handling lean correctly there)

[Eric Rodriguez]

The screenshots remind me of Freek's list!

[Eric Wieser]

It's not at all clear to me how you plan to scale from the 100 theorems list to mathlibs's 110k, but it's at least believable that some combination of ai guessing and human curation could do a reasonable job!

[Jireh Loreaux]

@John Mercer I will second Eric's comment above. These few screenshots communicate more than anything else you've said (in my opinion). Advertising these on the website I think is essential. Or maybe curating even better ones.

[John Mercer]

Jireh Loreaux said:

John Mercer I will second Eric's comment above. These few screenshots communicate more than anything else you've said (in my opinion). Advertising these on the website I think is essential. Or maybe curating even better ones.

Thank you so much everyone for the feedback! I've attached a Homer Simpson "DOH!" emoji here, if admins want to add it to the emoji list. I sure could use it right now! :joy: :doh:
9235-homer-doh.png

[John Mercer]

Hi all,

Providing a quick update!

1. New release of the site this week with all the feedback (e.g. screenshots @Jireh Loreaux !) and incorporating the bounty system feedback behind-the-scenes.
2. Included is a'Get Involved' page with the new Founding University Partner (FUP) program based on feedback from the wider math community (and a few that reached out from here!). Already signed University of Maryland and in talks with many others :rocket: If you're a tenured professor and want to schedule time to discuss, you can do so directly from the website.
3. The FUP program discussions have slowed waitlist batch entry a bit, but thanks to all those that signed up, and working hard to get you in on time.

Best,
John

[John Mercer]

Eric Wieser said:

It's not at all clear to me how you plan to scale from the 100 theorems list to mathlibs's 110k, but it's at least believable that some combination of ai guessing and human curation could do a reasonable job!

Hi @Eric Wieser apologies didn't respond to this directly. Already scaled well beyond 100 theorems, I listed above the sources of content ingestion above (math and cs arXiv, wikiproofs, etc). Think of this as the seed of the platform, and that positions us to mature via refining ingestion jobs and the bounty system. Perhaps I wasn't clear before: the bounties are for both formal and informal content, e.g. "fix the latex for the Atiyah–Segal completion theorem statement, and provide the latex for the original 1961 and general case from Graeme Segal in 1969" <- that's an example bounty.

[John Mercer]

Eric Rodriguez said:

The screenshots remind me of Freek's list!

Thanks @Eric Rodriguez , I was excited to see Freek follow us on Twitter lol.

[Eric Wieser]

Eric Wieser said:

(I'm sure you're aware, but it looks like your syntax highlighter isn't handling lean correctly there)

Note that this is still true in the new screenshots!

[John Mercer]

Gotcha @Eric Wieser thanks , it's in the backlog right now waiting for sprint entry (might be there for a bit given other priorities).

[John Mercer]

@Eric Wieser I've been following lean4 and mathlib4 channel and made sure I wasn't missing something in github wikis. Is there any knowledge base with artifacts for process and roadmap for mathlib4? Planning, prioritization, scoping and sunsetting timeline? I'm using and developing all on mathlib3 (e.g. a LeanGPT based on that corpus) but my concern and uncertainty is growing wrt the dependency of transitioning to lean4. What do the maintainers recommend for people developing on top of the lean ecosystem? (I posted on this thread vs other channels because it's a pertinent to my dependencies so if there's a better place please let me know). Related, is there a list of most valuable NLP tasks, analyses, and modeling that would be helpful to all during the migration?

[Eric Wieser]

If your goal is to build new sets of tools, and you don't care about having all of mathlib available to you immediately, then the right place to be is definitely Lean 4. The only thing that might be relevant to you is that none of the list of Freek's 100 problems (which you included in a screenshot) is ported yet; but I would guess that will change very soon

[Johan Commelin]

Is really none of them ported?

[Moritz Firsching]

https://github.com/leanprover-community/mathlib4/blob/c639b48cbbeedd2e3ecc46ec6a68d087a93f4189/Mathlib/Geometry/Euclidean/Sphere/Power.lean#L22

[Moritz Firsching]

https://github.com/leanprover-community/mathlib4/blob/c639b48cbbeedd2e3ecc46ec6a68d087a93f4189/Mathlib/Data/Nat/Digits.lean#L28

[Moritz Firsching]

at least two of them are

[Eric Wieser]

Sorry, I got confused; I meant none of the ones in archive are ported!

[Scott Morrison]

@John Mercer I'm not sure exactly information you're looking for (and likely it doesn't exist, we're still pretty uncertain about the sunsetting process). But I would wager there is a 50% chance that mathlib3 will be archived within 3 months. (And hope that it is less...)

[Johan Commelin]

To clarify, Scott hopes it is less than 3 months (not less than 50%).

[John Mercer]

Thanks all! That's really helpful. Freek's list is not a dependency, those are in the screenshot because they were the first ingested (so they show up first in a select *)

[John Mercer]

Hi everyone, wanted to let you know TMGP is now publicly available!

Based on your feedback, and that of the wider math community, you'll notice we've separated the concerns of mathlib infrastructure (and all open-source formal language repos) and aimed to democratize higher mathematics with the 1st marketplace and social platform for mathematical proof curation, writing, and formalization.

Our bounty system is akin to the"formalization projects" mentioned in the thread about Prolific (paid research study participation), but ours is more P2P marketplace (and of course specialized for math! :)).

There is a ProofChat Pro SaaS subscription available, but it's using APIs and we're still working on a LeanChat that is better than Copilot (If anyone is interested in working on this with me, let me know!).

Ok, that's enough for here - there is a tour of the product after you login. Hope you can kick the tires and look forward to your feedback! Any feature requests that can improve the experience to support and promote formalization projects within the Lean community and other formal communities are welcome.

image.png

[Bulhwi Cha]

Can I look around your bounty system without having to log in?

[David Loeffler]

John Mercer said:

Hi everyone, wanted to let you know TMGP is now publicly available!

Is there a mechanism for users to edit theorem statements (or suggest edits)? I looked at a few of the not-yet-proved theorems in number theory, and most of the theorem statements are just bare formulae. In some cases these do communicate the gist of the theorem, but very often they don't. Are you hoping to harness community feedback to knock these into shape?

[John Mercer]

David Loeffler said:

John Mercer said:

Hi everyone, wanted to let you know TMGP is now publicly available!

Is there a mechanism for users to edit theorem statements (or suggest edits)? I looked at a few of the not-yet-proved theorems in number theory, and most of the theorem statements are just bare formulae. In some cases these do communicate the gist of the theorem, but very often they don't. Are you hoping to harness community feedback to knock these into shape?

Hi @David Loeffler thanks so much for the question!

Right now, to edit a statement or proof that you didn't create, you have to join the committee. Any committee member can edit the statement and proofs (informal/formal). I also think of the committee as the managers/owners of the statement page, but that dual meaning is not clear in the UX right now.

I've thought about a statement.owner that would populate the "Managed by [profile]" similar to the "Created by [profile]" that show up on the page. And that one person could also be elected by committee members.

We're about to have a serious programmatic injection of conjectures and theorems (the actual LaTeX statements and proofs) from arXiv papers. So related to above, the natural default designation of the committee members are the authors of that paper (e.g. to tidy up and make sure the statement LaTeX is correct, and make decisions about proof acceptance etc). Any thoughts on how to be judicious about the most wanted/valuable papers in arXiv would be wonderful! (using the arxiv bulk data access and doing all the munging with latex files)

Finally, I'm a little embarrassed about the layout of the View page right now. We're in serious need of a design iteration to better organize and navigate the different sections now. For example, the statement location and real-estate isn't ready handle longer statements. Same goes for the informal proof, and handling multiple alternative longer proofs.

Would love any recommendations in how you'd like to see the options/features above implemented.

[David Loeffler]

Hi everyone, wanted to let you know TMGP is now publicly available!

I think the underlying logical model used by this website does not match how mathematicians think about theorems. Mathematics isn't just a list of theorems, each with its own separate proof, any more than a building is a list of separate bricks: it matters how you put the bricks together, and which bricks rest on which others.

So, for instance, the "Lean proof" of Euler's summation of 1 / n ^ 2 given in the database is just 3 lines. But those 3 lines, quoted from zeta_values.lean in mathlib3, are just plugging k = 2 into a general formula for sum (1 / n ^ k) for all even k. The real work lies in the other theorems and lemmas quoted in those 3 lines, and in the lemmas they quote in turn, etc, until you realise that the full proof involves many tends of thousands of lines distributed across half the files in the mathlib library. So saying that those 3 lines "are" the proof is rather dubious, and arguing that the writer of those 3 lines deserves financial credit for proving the theorem is even more so (as if you would pay 100% of the cost of building a house to the one roofer who fits the last tile at the roof crest).

[Bolton Bailey]

And yet, isn't this how it sometimes works in traditional mathematics? The most prominent example I can think of of a mathematician being awarded a monetary prize for their math is Perelman, who turned down the prize, saying it was unfair for the very reason that the work of proving the Poincare conjecture was partly done not by him.

[Bolton Bailey]

I think the question of setting up an incentive structure for math is an interesting and hard problem. It would be nice if, when we had a prize to award for a particular theorem, it could be evenly distributed over all the contributors to lemmas for that theorem. The trouble I had when trying to turn this into a sensible design was that an attacker could just re-prove or slightly modify whatever lemmas they needed and claim all of the prize. I wasn't really able to solve this issue, unfortunately, (if anyone has thoughts on this, I'd be interested in hearing them).

[Bolton Bailey]

@John Mercer I don't really get some of the interface. Descartes rule of signs for example, has a checkmark for "formally proved", but none of the formal proof tabs have any contents.

[Bolton Bailey]

Also, there's "the ballot problem" and "Bertrand's ballot theorem" are these the same thing?

[Bolton Bailey]

Is it intended that all the entries in the site are theorems, or is it ok to put open questions up as well? It seems more likely that someone would want to put up a bounty on an open question.

[Bolton Bailey]

If so, is there a way to put a bounty on deciding a problem one way or another, rather than just putting two separate bounties on both the proposition and its negation?

[John Mercer]

Bolton Bailey said:

Is it intended that all the entries in the site are theorems, or is it ok to put open questions up as well? It seems more likely that someone would want to put up a bounty on an open question.

Hi @Bolton Bailey , if you start typing "conj" in the search bar you'll see all the conjectures filtered. We'll be adding a type field on statements for definition, proposition, lemma, theorem, conjecture categories and that will be another advanced search option to filter.

[John Mercer]

@David Loeffler didn't forget about you! Just a longer response is needed and want be thoughtful. Thanks for your patience, targeting tomorrow evening Sat latest.

[Junyan Xu]

I think the question of setting up an incentive structure for math is an interesting and hard problem. It would be nice if, when we had a prize to award for a particular theorem, it could be evenly distributed over all the contributors to lemmas for that theorem. The trouble I had when trying to turn this into a sensible design was that an attacker could just re-prove or slightly modify whatever lemmas they needed and claim all of the prize. I wasn't really able to solve this issue, unfortunately, (if anyone has thoughts on this, I'd be interested in hearing them).

I have some thoughts about this:

1. After a formalization request with bounty is completed and the winning formalization publicized, there could be a period during which anyone can suggest golfs (minimizing a weighted sum of compile time and length of proof) and eat away a part of the bounty (say 20% of the proportion reduced, so 2% of the bounty if proof shortened by 10%, or 10% of the bounty if shortened by half). This (and also competition to be the first) incentivizes competitors to use as much of mathlib as possible to shorten the proofs. (The golfs could be restricted to using the mathlib version when the bounty was announced.)

2. When setting up the bounty, a fixed amount can be reserved for contributors of mathlib declarations used (transitively) in the winning formalization, and the winning formalizers only get the remaining bounty. This incentivizes competitors to add their contribution to mathlib when appropriate, but creates some conflict of interest for mathlib maintainers / reviewers. Even if your didn't win the race, if you're able extract more general lemmas, they have better chances entering mathlib.

The question remains how to assign credits to declarations and contributors of a declaration.

3. I'm inclined to assign the mathlib part of the bounty to declarations in proportion to their lengths (including proofs). However, tactics could drastically reduce lengths and some declarations are generated by tactics (e.g. to_additive), so special credits should be given to tactic authors. Another problem is that foundational declarations (like natural numbers, real numbers, groups and rings) will get used a lot in any formalization, so maybe we need to adopt ClopenAI's "capped profit" model (say $1,000 max for each declaration), or we may downweight each declaration by its PageRank in mathlib: if a declaration is used a lot in mathlib, it also get more chances to be used transitively, so it seems fair that it be downweighted more. Here's a 2015 paper using PageRank for theorem proving.

4. Assigning credits to individual contributors to a declaration can be even more tricky; even though we have tools like git blame and mathlib changelog to track changes to a declaration, it's still probably the hardest step to automate, and it's nonobvious how to assign credits to golfs, refactoring, and porting.

5. Should competitors publish formalizations on a blockchain to avoid a centralized authority determining priority / declaring winner? Charles Hoskinson may be happy with this ... and this also encourages shorter formalization.

[John Nicol]

Junyan Xu said:

1. After a formalization request with bounty is completed and the winning formalization publicized, there could be a period during which anyone can suggest golfs (minimizing a weighted sum of compile time and length of proof)...<snip>

2. I'm inclined to assign the mathlib part of the bounty to declarations in proportion to their lengths (including proofs). However, tactics could drastically reduce lengths and some declarations are generated by tactics (e.g. to_additive), so special credits should be given to tactic authors...<snip>

There's certainly a use in reducing assumptions in a proof, or making theorems more powerful (weakening, generalizing, etc.)

But what is the (mathematical) advantage in golfing proof length in Lean by using more powerful tactics? It seems these just make proofs harder to read and comprehend. Reducing compile time is nice, but it seems this could be done more effectively by targeting the underlying system.

[Johan Commelin]

I think Junyan is suggesting that step so that people can sniff out duplicate lemmas. Otherwise a proof auther can claim to have done 79% of the work, by just duplicating a lot of mathlib. But with this extra step, people can reduce that to 19%, by showing that many of the lemmas are just coming from mathlib... you get the point

[Yury G. Kudryashov]

Will this create a pressure on adding trivial lemmas to, e.g., Data.Set.Basic and using them in a tactic?

[Bolton Bailey]

Junyan Xu said:

After a formalization request with bounty is completed and the winning formalization publicized, there could be a period during which anyone can suggest golfs (minimizing a weighted sum of compile time and length of proof) and eat away a part of the bounty (say 20% of the proportion reduced, so 2% of the bounty if proof shortened by 10%, or 10% of the bounty if shortened by half). This (and also competition to be the first) incentivizes competitors to use as much of mathlib as possible to shorten the proofs. (The golfs could be restricted to using the mathlib version when the bounty was announced.)

This is interesting, but my concern is that this will incentivize obfuscation: There will be a generic program that complicates your proof so much that it's impossible to simplify. It seems related to the cryptographic primitive of indistinguishability obfuscation.

[Bolton Bailey]

I definitely like the suggestion that there should be incentive to add theorems/lemmas to mathlib. Thinking of the "problem-solving"/"theory-building" division in mathematical personality, it seems unfair that one should get credit and not the other.

[Yury G. Kudryashov]

Who gets credit for docs#Set.image_subset_iff ?

[Yury G. Kudryashov]

Or, to make things a bit more complicated, for docs#map_mul ? We had a version for unbundled homs with a typeclass assumption long before bundled homs were added.

[Yury G. Kudryashov]

Once you turn writing such files into a form of a passive income, you get a lot of problems.

[Junyan Xu]

@Yury G. Kudryashov Your two examples are what I mean by "foundational declarations" in my point 3, where I suggested to address the issue by "capped profit" or downweighting by PageRank. docs#map_mul could potentially be traced back to the unbundled version via mathlib changelog, and the example touches on the issue of assigning credit to refactors, which I identified as tricky to automate. My ideas are preliminary, may contain many loopholes, aren't proven to work in practice, and are meant for eliciting discussions. More thought experiments and suggestions from the community are very welcome!

@Bolton Bailey Yeah, it seems my point 2 better addresses the issue you raised, and point 1 merely ensures mathlib declarations get their fair credits, and the bounty winner doesn't have much power to dictate which declarations get the mathlib part of the bounty. The mathlib part of the bounty (or maybe "royalty"?) would be fixed when the bounty was announced, and the bounty winner can only dip into it by adding (part of) their formalization to mathlib. Whether mathlib should receive a fixed percentage, a fixed amount, or any amount that the bounty offerer prefers is a question open to debate.

(Update: I realize I didn't actually address the obfuscation issue. I think it's a valid concern, but it remains to be seen how well obfuscation attack work in practice for formal proofs. It seems indistinguishability obfuscation is not yet practical, and obfuscation may hurt performance (compile time in our case) and lengthen proofs to some extent. There will be incentive to develop de-obfuscation tools as well (possibly employing LLMs like ChatGPT) to claim part of bounty via golfing).

[Mac Malone]

Junyan Xu said:

When setting up the bounty, a fixed amount can be reserved for contributors of mathlib declarations used (transitively) in the winning formalization, and the winning formalizers only get the remaining bounty.

This seems counter-intuitive to me. When a bounty is offered for a project, the goal is generally to inspire new work, not reward existing work. Thus, I would expect the bounty to only award contributors to the (formalized) "new math" needed for a theorem and not be given for old definitions.

[Mac Malone]

This would also solve a number of problem of determine credit for deeply nested basic (and very old) definitions.

[Anatole Dedecker]

I have nothing interesting to add to this discussion, but I just wanted to note that all these issues are basically why researchers aren't paid on a "per article" basis (at least in theory), and also why publicly-funded research even exists in many countries. So I wouldn't say this is really a formalization problem, I just don't think that these kind of principles are applicable anywhere in math. And indeed the Perelman example shows that too.

[Bolton Bailey]

Junyan Xu said:

5. Should competitors publish formalizations on a blockchain to avoid a centralized authority determining priority / declaring winner? Charles Hoskinson may be happy with this ... and this also encourages shorter formalization.

I imagine Hoskinson is already aware of the idea - see Qeditas from IOHK. I'm not sure if this project went anywhere though.

[Bolton Bailey]

Yury G. Kudryashov said:

Who gets credit for docs#Set.image_subset_iff ?

Well, git blame tells me it would be Scott Morrison :grinning_face_with_smiling_eyes:

[Bolton Bailey]

I guess the more principled answer is "whoever first wrote the form of that lemma which is easiest to integrate into a golfed version of whatever the final theorem is".

[Bolton Bailey]

I agree with Mac though that if any version of this "works" then it would probably work better if we just took mathlib lemmas before some date for granted and didn't assign any credit to them.

[Adam Topaz]

git blame doesn’t give the right answer in mathlib4, right?

[Bolton Bailey]

True. This makes me wonder - what will become of the mathlib leaderboard when we transition?

[Adam Topaz]

For the leader board we could come up with some combination of stats from ml3 before tomorrow, and ml4 after tomorrow (tomorrow is the freeze).

[Adam Topaz]

But those stats don’t need to be as granular as what’s being discussed above

[Eric Wieser]

Merging the git histories would result in the dashboard being continuous across the port

[Adam Topaz]

How hard is it to merge histories?

[Eric Wieser]

Trivial

[Adam Topaz]

Oh great

[Eric Wieser]

But we only get to do it once, so should think carefully about what we want the result to look like

[Adam Topaz]

Nice to have some git gurus around ;)

[Eric Wieser]

There's no need to do it immediately after the freeze though; it can be done retrospectively in a way that still makes sense. See my thread elsewhere...

[Adam Topaz]

But merging histories still doesn’t change the git blame issue, right?

[Eric Wieser]

That's what the "carefully" comes down to

[Eric Wieser]

When we create the merge we can probably pick whether we want the porting history by default or the ml3 history

[Joseph Myers]

Junyan Xu said:

1. After a formalization request with bounty is completed and the winning formalization publicized, there could be a period during which anyone can suggest golfs (minimizing a weighted sum of compile time and length of proof) and eat away a part of the bounty (say 20% of the proportion reduced, so 2% of the bounty if proof shortened by 10%, or 10% of the bounty if shortened by half). This (and also competition to be the first) incentivizes competitors to use as much of mathlib as possible to shorten the proofs. (The golfs could be restricted to using the mathlib version when the bounty was announced.)

Golfs aren't always a good idea; for example, if a proof is made shorter by abusing defeq rather than making proper use of the relevant API.

Using as much of mathlib as possible isn't always a good idea; sometimes reduced dependencies are desirable to improve parallelism for partial rebuilds after changes, or because for other uses it's convenient for file B to import file A rather than the other way round.

Restricting anything to "the mathlib version when the bounty was announced" is definitely a bad idea. The collaborative goal is to build a highly integrated library of mathematics, and it's important that any incentives are aligned to that goal rather than encouraging individuals to do something that gets more of a bounty but is suboptimal for the longer-term development of the library (for example, that suggests it would be a bad idea to reward work that hasn't got into mathlib - which may take years after initial implementation - and that doing the work to get something into mathlib is at least as important as the initial formalization). Often work needs major refactors between when something is first formalized and when it's ready to go in mathlib; sometimes it may be reimplemented several times, with the earlier implementations possibly being of value in exploring possible approaches to an area even if no code of them ended up being used (so just looking at what code ended up in mathlib isn't a sufficient way to assess value either); all those refactors and reimplementations should be able to depend on subsequent developments in mathlib, which may well have been done specifically to facilitate such as redesign of the original formalization.

[Mac Malone]

Joseph Myers said:

The collaborative goal is to build a highly integrated library of mathematics, and it's important that any incentives are aligned to that goal rather than encouraging individuals to do something that gets more of a bounty but is suboptimal for the longer-term development of the library (for example, that suggests it would be a bad idea to reward work that hasn't got into mathlib...)

That may be mathlib's goal (and quite rightly), but I imagine the website's goal is different. The website seems catered towards customers who want something formalized paying whoever will do so to get a formally checked result however they can. Thus, it does not seem like integration with mathlib would be a priority (from the website's perspective), though I certainly imagine Lean results will still end up at least using mathlib.

[Bolton Bailey]

Joseph Myers said:

Restricting anything to "the mathlib version when the bounty was announced" is definitely a bad idea.

I assumed the point of the suggestion to make the payouts depend only on the mathlib version when the bounty is announced is to try to prevent potentially bad incentives from adversely affecting mathlib development. For example - we wouldn't want people advocating for refactors which would be bad on the whole, but which make their own proof simpler and thereby entitle them to a greater reward. I'm not sure whether this is a bigger or smaller concern than the idea that people will avoid contributing to mathlib in the hopes of getting a reward for their contribution later, but feels a bit more pernicious.

[John Mercer]

David Loeffler said:

Hi everyone, wanted to let you know TMGP is now publicly available!

I think the underlying logical model used by this website does not match how mathematicians think about theorems. Mathematics isn't just a list of theorems, each with its own separate proof, any more than a building is a list of separate bricks: it matters how you put the bricks together, and which bricks rest on which others.

So, for instance, the "Lean proof" of Euler's summation of 1 / n ^ 2 given in the database is just 3 lines. But those 3 lines, quoted from zeta_values.lean in mathlib3, are just plugging k = 2 into a general formula for sum (1 / n ^ k) for all even k. The real work lies in the other theorems and lemmas quoted in those 3 lines, and in the lemmas they quote in turn, etc, until you realise that the full proof involves many tends of thousands of lines distributed across half the files in the mathlib library. So saying that those 3 lines "are" the proof is rather dubious, and arguing that the writer of those 3 lines deserves financial credit for proving the theorem is even more so (as if you would pay 100% of the cost of building a house to the one roofer who fits the last tile at the roof crest).

@David Loeffler As promised couple days ago (although now I hate to interrupt a great bounty discussion!).

"I think the underlying logical model..."

Aside from the need for a similar international consensus to the HGP needed to rectify how we store, organize and execute the development lifecycle of mathematics, there is a reason I chose TMGP as a name. And it's the same reason we don't need a new house analogy.

Phenotypes don't emerge because of a list of genes - but from complex cell circuitry of molecular interactions. Nevertheless, you have to start with the standardized map of the genes (from a global mathematics research perspective), hence TMGP. The topology of the network of math vs biology is fundamentally different, because it's a tree structure, as you've alluded to.

So just because you see a table when you login today, doesn't mean that's the end game.

TMGP is not intended to merely be the google search of statements but a way to navigate -- in real time -- the proof space (so more like google maps). This is both for individual proof searches as your navigating alternative paths in a proof tree, but also to give us insight into the global architecture of our current knowledge of the proof space for real time empirical metamathematics. (From a research perspective, this is what I'm most interested in: how properties of axiomatic systems dictate and constrain the architecture of the resulting proof spaces).

But again, from a product development perspective, we have to start with the informal statements (nodes) and then compute the edges, along with ontology efforts that go with that.

"So, for instance, the "Lean proof" of Euler's summation...."

I understand this as well, and I empathize that perhaps some of the feedback is because of feelings that TMGP is not reflecting the reality of mathlib or it's development nuances. It's one of the reasons I focused on the marketplace and prioritized informal. Separation of concerns.

In some ways, you have to turn off your formal math brain and squint your eyes as there will be releases that are more approximate stepping stones. When this happens, just consider it a sorry; that needs fleshing out, and then would appreciate constructive suggestions for refinements/enhancements.

[Junyan Xu]

This seems counter-intuitive to me. When a bounty is offered for a project, the goal is generally to inspire new work, not reward existing work. Thus, I would expect the bounty to only award contributors to the (formalized) "new math" needed for a theorem and not be given for old definitions.

I think people interested in seeing mathematics formalized will recognize the centrality of mathlib, specifically that a more complete mathlib would make future formalization projects easier and cheaper; in particular it would allow them to state more of their formalization targets. (I'd expect each bounty challenge to consist of exactly one proposition to be proved without sorried definitions; I'd like to add to a bounty for CFSG but I don't think the statement is formalized anywhere yet (but this may be achievable via several bounties with specifications for each family of FSG and each sporadic FSG). BTW, not sure if it puts any pressure on Mochizuki and co., but I'd like to add $100 to a bounty for a formal proof of the ABC conjecture (which has a simple statement).)

I also expect that people may have preference in certain areas of mathematics and specifically want to encourage mathlib development in those areas, and rewarding declarations that are actually used to prove their targets is a natural way to achieve this.

I have nothing interesting to add to this discussion, but I just wanted to note that all these issues are basically why researchers aren't paid on a "per article" basis (at least in theory), and also why publicly-funded research even exists in many countries. So I wouldn't say this is really a formalization problem, I just don't think that these kind of principles are applicable anywhere in math. And indeed the Perelman example shows that too.

It's hard to track evolution of ideas or dependencies among publications in mathematical research, but a formal library / codebase makes it easy to track dependency. It's hard to track how many times a function in typical open-source software is called in the wild, but it's easy to count how many times a declaration is used in a published formal proof.

It seems it's generally agreed that rewarding mathlib contributions is a good idea, but I agree with Anatole that assigning reward "per article/declaration" may not be the ideal solution. Since TMGP is aiming to become a social network, community decision making should be possible, but objective metrics will still be valuable. The metrics might be passed into an LLM for a more holistic judgment/arbitration that takes into account the Git history (including refactors and golfs etc.), PR comments, and Zulip coordination.

Formalization of mathematics is a nascent practice and does involve a lot of research at the current stage, but it's also largely an engineering problem (we're even constantly tweaking Lean core!). I think bounties will not only attract researchers/mathematicians but also industrial players, and incentivize them to leverage their proprietary LLMs and develop powerful tools on top of them. (I doubt Google's LaMDA, Flamingo, Minerva etc. were used much externally, but Med-PaLM is likely going to be different.) Reserving a portion of bounties for mathlib would encourage them to put potentially messy auto-generated proofs in an organized form suitable for mathlib.

I agree with Mac though that if any version of this "works" then it would probably work better if we just took mathlib lemmas before some date for granted and didn't assign any credit to them.

This sounds reasonable but is there a natural cutoff date? Was there a specific date when mathlib "went public" (open to unsolicited contributions)?

[Junyan Xu]

@Joseph Myers I have trouble understanding the criticisms in your last paragraph; I think my point 2 (reserving part of bounty for mathlib) is exactly to encourage contributions to mathlib, whether for the reserved portion of the current bounty or of future bounties.

I wanted to restrict the golfers to use only the mathlib version when the bounty was announced, because the bounty competitors can't anticipate future mathlib development when they started working on the bounty target, and it would put unnecessary burden on them to keep track of latest mathlib development. However, I realized that this may not be practical, as a long time (several years) may have passed when the target is completed. So maybe we could restrict golfers to whatever mathlib version the bounty winner uses, or the version (say) one month earlier from completion.

As I said, the bounty competitors have the option to PR appropriate parts of their formalization to mathlib in order to claim a part of the reserved bounty (and the parts that enter mathlib need not / will not be over-golfed). This might partially divulge what they are doing, but if the PR is merged (say) one month before other competitors complete the challenge, the winner may not be able to avoid using the declarations added in the PR without being golfed.

However, we can't guarantee speedy review of PRs, and one month may be too long. I think we should allow the bounty winner to make PRs after the target is completed and determine when to distribute the reserved bounty: they can wait until all their PRs are merged to claim as large a portion of the reserved bounty as possible.

[Bolton Bailey]

Junyan Xu said:

This sounds reasonable but is there a natural cutoff date? Was there a specific date when mathlib "went public" (open to unsolicited contributions)?

In some sense, the start of this conversation is the natural cutoff date, since I don't think that mathlib contributors would have had any reason to think they were going to be compensated monetarily before. Probably they still don't - I don't think anyone has been reading this conversation and thinking "I should probably stop making mathlib PRs because I might want to use my lemmas as Intellectual property later". But if it ever does get to the point where people are choosing not to contribute for this reason, then that would be a good time to try and allow mathlib contributions to get credit, so that mathlib's growth can be boosted rather than hampered by this bounty system.

[Scott Morrison]

That would be a terrible outcome. In fact, I have trouble seeing any success of a monetary bounty system as a positive contribution towards mathematics, formalization, or mathematics research, but I am sufficiently skeptical of any such system ever gaining traction that I'm not concerned about this.

[Mario Carneiro]

This sounds reasonable but is there a natural cutoff date? Was there a specific date when mathlib "went public" (open to unsolicited contributions)?

The direct answer to this question is "day 1", mathlib has been developed completely in the open source from the beginning and has accepted unsolicited contributions the whole time. Besides this, drawing an arbitrary cutoff in the middle is rude to all those who developed the foundational material beforehand without which all the advanced stuff couldn't exist.

[John Mercer]

Bulhwi Cha said:

Can I look around your bounty system without having to log in?

hi @Bulhwi Cha , We're planning on opening up the Search/View to public. Then, you only have to login if you want to participate. We are finishing a sprint right now, and it's planned for the next sprint (so ~ 2 weeks).

[John Mercer]

Hi all,

A new MGP release is out. The new tour will walk you through all the features at login, but I’ll highlight a few things here.

Our goal with this release is to go from neat concept illustration to a more intuitive, functional and generalized platform for both peer-to-peer and institutional grant funding that accelerates mathematical discovery by leveraging the power of a broader community.

Updates

Projects: You can now visualize the project status checklist for each statement, and the current open projects for each statement (open to both submissions and funding). Let us know what you think! We wanted to demystify and answer the question “So what can I do?!”

Search: More advanced search options for different statements, and a summary progress bar in the search results table to help you quickly assess where you can make an impact.

Creation: Revamp of the Statement creation page that lets you add expository notes, references and even a YouTube link for an explainer video. We have one, and possibly two, new entries coming online that include an explainer video on the history of the open problem being funded.

Teams: You can now form teams, and submit projects on behalf of a team. The team can decide how grant award %'s should be allocated to each teammate, and the team leader can make the allocations.

Dashboard: The new dashboard lets you quickly see platform stats and find the most popular statements, grant activity and most recent activity.

About Page: Not exciting from a feature perspective, but it was in desperate need of an update to help people understand the mission we're on.

Along with this, we have what is shaping up to be over $10,000 in new grants coming on line in the coming weeks and our goal is to get to $1,000,000 in grants this year to fund curation (for known math), new proofs/solutions, and formalization projects in Lean, Coq, HOL, and Metamath.

One other thing you'll notice is that we've departed from using the term "bounty."

And finally a BIG thank you to everyone in this thread that provided feedback. The grant award allocation functionality (team formation and defining % awards across team members) was based on your feedback and reinforced what we heard from the broader math community.

Any questions or comments please let me know.