Xiamen University Malaysia LEAN Group: Seeking to Contribute

Stream: mathlib4

[math.xmum]

Hi,

Here‘s Wang Haocheng. On behalf of our group, I will introducing our LEAN Group from the Department of Mathematics at Xiamen University Malaysia.

Our group includes three undergraduate students who have been into mathematical formalization and proofs since August 2023, and our supervisor Dr. Ma Jiajiun. In less than a year, we've tackled major sections of game theory formalization with some accomplishments.

Key Highlights of Our Work

Completed Tasks
- Auction Theory: Including formalized proofs on no-dominant strategies in first-price auctions, the DSIC (Dominant Strategy Incentive Compatible) mechanisms, and non-negative utility in second-price auctions.
- Myerson's Lemma: Optimal auctions addressing a wide range of auction design problems for sellers.
- Topological Standard Simplex is Compact

Work-in-Progress:
- Minimax Theorem: Von Neumann's foundational theory in game theory and mathematical economics.

Planned Tasks:
- Loomis' Theorem
- Brouwer's Fixed Point Theorem
- Nash's Existence Theorem

We are now looking to create a new branch where we can contribute our formalized codes to Mathlib.

We would be thrilled to discuss this initiative with the community and explore possibilities for collaboration and support. Please feel free to respond here.

Our repository: zerosum: This is an open-source project dedicated to providing a foundation of game theory concepts in Lean 4. (gitee.com)

We are excited about the opportunity to grasp the spark and grow with you guys. :smiley:

[Josha Dekker]

Very nice to hear, welcome! I think these are very nice results to have formalised. Whether these are all in the scope of Mathlib I will leave up to others to decide, but I'd like to bring two things to your attention:

• Topological Standard Simplex is Compact is isCompact_stdSimplex in Mathlib
• There is https://github.com/asouther4/lean-social-choice, which formalises some results from Social Choice Theory

[Johan Commelin]

Welcome! Looking forward to more discussions and collaborations. I will point out that Brouwer's fixed point theorem has also been formalized in Lean 3 by Brendan Seamas Murphy (but is not yet in mathlib).

[math.xmum]

Thank you for the warm welcome and for supportive pointing out the previous formalization of Brouwer's Fixed Point Theorem by Brendan Seamas Murphy in Lean 3. Looking forward to engaging in more discussions and exploring potential collaborations with you and the author @Brendan Seamas Murphy . :grinning_face_with_smiling_eyes:

[math.xmum]

Josha Dekker said:

Very nice to hear, welcome! I think these are very nice results to have formalised. Whether these are all in the scope of Mathlib I will leave up to others to decide, but I'd like to bring two things to your attention:

• Topological Standard Simplex is Compact is isCompact_stdSimplex in Mathlib
• There is https://github.com/asouther4/lean-social-choice, which formalises some results from Social Choice Theory

Thank you very much for the warm welcome and for recognizing our formalization work! I believe that the task of proving theorems in game theory is a serious mathematical endeavor. A key resource guiding our efforts is the textbook "Mathematical Foundations of Game Theory" by Rida Laraki, Jerome Renault, and Sylvain Sorin, is what we are working with. You can access this textbook here for a deeper understanding of the mathematical theorems we strive to formalize.
https://doi.org/10.1007/978-3-030-26646-2

[math.xmum]

:working_on_it:

[math.xmum]

Johan Commelin said:

Welcome! Looking forward to more discussions and collaborations. I will point out that Brouwer's fixed point theorem has also been formalized in Lean 3 by Brendan Seamas Murphy (but is not yet in mathlib).

Thank you for the warm welcome and for supportive pointing out the previous formalization of Brouwer's Fixed Point Theorem by Brendan Seamas Murphy in Lean 3. Looking forward to engaging in more discussions and exploring potential collaborations with you and the author @Brendan Seamas Murphy .

[Yaël Dillies]

@Yury G. Kudryashov and I also have plans to formalise Brouwer in a different way. It will probably happen this summer

[Ma, Jia-Jun]

Yaël Dillies said:

Yury G. Kudryashov and I also have plans to formalize Brouwer in a different way. It will probably happen this summer

Do you plan to prove via Sperner's lemma? This is also our plan. Before the actual proof, one has to build some part of the theory of abstract simplicial complex. This is a group of students at the National University of Singapore working on it now.

[Floris van Doorn]

One of my students (@Joshua Wirtz) formalized the implication Brouwer's fixed point theorem -> existence of Nash equilibria here: https://github.com/wjrtz/LeanCourse23/blob/master/LeanCourse/Project/game_theory.lean

[Ma, Jia-Jun]

Floris van Doorn said:

https://github.com/wjrtz/LeanCourse23/blob/master/LeanCourse/Project/game_theory.lean

Hi Floris, It is great to know that this step has been down.:tada: On the other hand, I can not access the repo you posted, maybe because it is a private repo.

[Yury G. Kudryashov]

@Yaël Dillies With my new job, I have very little time for Mathlib. So, if something from my unwritten list of things I want to see formalized will be formalized by someone else, I will be happy to see this.

[Floris van Doorn]

Ma, Jia-Jun said:

Floris van Doorn said:

https://github.com/wjrtz/LeanCourse23/blob/master/LeanCourse/Project/game_theory.lean

Hi Floris, It is great to know that this step has been down.:tada: On the other hand, I can not access the repo you posted, maybe because it is a private repo.

Oh, you're right. I can ask the student if I can make his work public.

[Joshua Wirtz]

This repository is private, because it contains some personal information. I just made the formalization public at https://github.com/wjrtz/lean_game_theory

[Eric Wieser]

Can you add the lakefile, lake manifest, and Lean toolchain to that project too? Otherwise it will quickly become dead code that no one else can run!

[Joshua Wirtz]

Eric Wieser said:

Can you add the lakefile, lake manifest, and Lean toolchain to that project too? Otherwise it will quickly become dead code that no one else can run!

Done!