From a10294f80a022bc455a16272ed097fe6e75a66ce Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Wed, 6 May 2026 19:50:47 -0400 Subject: [PATCH 1/5] Add queueboard reviewer interests to reviewer team page Fetches preferred labels and free-form notes from the queueboard API at build time (via QUEUEBOARD_API_URL repo variable) and displays them on the reviewer team page. Adds github field to People dataclass; people.yaml entries will need github usernames added to map API data to members. Co-Authored-By: Claude Sonnet 4.6 --- .github/workflows/build.yml | 1 + make_site.py | 13 ++++++++++++- templates/_team.html | 13 ++++++++++++- 3 files changed, 25 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 988dfe0eea..faf1e65bed 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -58,6 +58,7 @@ jobs: github_repo: ${{ github.repository }} github_ref: ${{ github.ref }} ZULIP_KEY: ${{ secrets.ZULIP_KEY }} + QUEUEBOARD_API_URL: ${{ vars.QUEUEBOARD_API_URL }} - name: Upload artifact id: upload-artifact diff --git a/make_site.py b/make_site.py index e186ee50bc..f589902f71 100755 --- a/make_site.py +++ b/make_site.py @@ -157,10 +157,20 @@ class People: name: str descr: str = '' img: str = '' + github: str = '' with (DATA/'people.yaml').open('r', encoding='utf-8') as m_file: peoples = {mtr['name']: People(**mtr) for mtr in yaml.safe_load(m_file)} +reviewer_data: dict = {} +_queueboard_url = os.environ.get('QUEUEBOARD_API_URL') +if _queueboard_url: + try: + with urllib.request.urlopen(_queueboard_url) as _resp: + reviewer_data = {r['github_login']: r for r in json.loads(_resp.read())['reviewers']} + except Exception as e: + print(f'Warning: could not fetch reviewer data: {e}', file=sys.stderr) + @dataclass class Team: name: str @@ -938,8 +948,9 @@ def read_md(src: str) -> str: env.filters={ 'url': url, 'md': render_markdown, 'tex': clean_tex } team_tpl = env.get_template('_team.html') for team in teams: + extra = {'reviewer_data': reviewer_data} if team.url == 'reviewers' else {} with (target/'teams'/(team.url + '.html')).open('w') as tgt_file: - team_tpl.stream(team=team, menus=menus, base_url=base_url).dump(tgt_file) + team_tpl.stream(team=team, menus=menus, base_url=base_url, **extra).dump(tgt_file) for folder in ['css', 'js', 'img', 'papers', str(target/'teams')]: diff --git a/templates/_team.html b/templates/_team.html index 7721ef450b..595abd787b 100644 --- a/templates/_team.html +++ b/templates/_team.html @@ -24,7 +24,18 @@
{{ member.name }}
{% else %} {% endif %} From 00ef234556f102938bda01967b6bd2899c0713bb Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Wed, 6 May 2026 19:55:23 -0400 Subject: [PATCH 2/5] change env var name --- .github/workflows/build.yml | 2 +- make_site.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index faf1e65bed..ac8ff2251c 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -58,7 +58,7 @@ jobs: github_repo: ${{ github.repository }} github_ref: ${{ github.ref }} ZULIP_KEY: ${{ secrets.ZULIP_KEY }} - QUEUEBOARD_API_URL: ${{ vars.QUEUEBOARD_API_URL }} + QUEUEBOARD_REVIEWER_INTERESTS_API_URL: ${{ vars.QUEUEBOARD_REVIEWER_INTERESTS_API_URL }} - name: Upload artifact id: upload-artifact diff --git a/make_site.py b/make_site.py index f589902f71..e543278069 100755 --- a/make_site.py +++ b/make_site.py @@ -163,7 +163,7 @@ class People: peoples = {mtr['name']: People(**mtr) for mtr in yaml.safe_load(m_file)} reviewer_data: dict = {} -_queueboard_url = os.environ.get('QUEUEBOARD_API_URL') +_queueboard_url = os.environ.get('QUEUEBOARD_REVIEWER_INTERESTS_API_URL') if _queueboard_url: try: with urllib.request.urlopen(_queueboard_url) as _resp: From d5b90d6145d558c5252f4007111adf679a895f20 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Thu, 7 May 2026 02:09:01 -0400 Subject: [PATCH 3/5] update people.yaml and teams.yaml --- data/people.yaml | 122 +++++++++++++++++++++++++++++++++++++++++++++-- data/teams.yaml | 2 +- 2 files changed, 118 insertions(+), 6 deletions(-) diff --git a/data/people.yaml b/data/people.yaml index 5a1614212e..a50d0cc7df 100644 --- a/data/people.yaml +++ b/data/people.yaml @@ -1,5 +1,6 @@ - name: Jeremy Avigad + github: avigad descr: | Jeremy is a Professor of Philosophy at Carnegie Mellon University (USA). He did a PhD in mathematical logic at Berkeley, and has @@ -8,6 +9,7 @@ img: jeremy.png - name: Anne Baanen + github: Vierkantor descr: | Anne is a mathematical research engineer at the Mathlib Initiative. They did a PhD on formalizing algebraic number theory at Vrije @@ -16,6 +18,7 @@ img: anne.jpg - name: Matthew Robert Ballard + github: mattrobball descr: | Matt is a Professor of Mathematics at the University of South Carolina (Columbia, USA). He did a PhD on derived categories in algebraic @@ -24,6 +27,7 @@ img: mrb.png - name: Reid Barton + github: rwbarton descr: | Reid is a post-doc at the University of Pittsburgh (USA). He did a PhD in algebraic topology in Harvard. He worked on the Glasgow @@ -32,6 +36,7 @@ img: reid.jpg - name: Riccardo Brasca + github: riccardobrasca descr: | Riccardo is an Associate Professor of Mathematics at Université Paris Cité (France). He did a PhD in number theory in Milan. He has @@ -39,6 +44,7 @@ img: riccardo.jpg - name: Kevin Buzzard + github: kbuzzard descr: | Kevin is a professor of pure mathematics at Imperial College London. He did a PhD under Richard Taylor in Cambridge UK. @@ -46,6 +52,7 @@ img: kbuzzard.jpg - name: Mario Carneiro + github: digama0 descr: | Mario is a post-doc at Carnegie Mellon University (USA). He did a PhD in pure & applied logic at CMU under Jeremy Avigad. He @@ -54,6 +61,7 @@ img: mario.jpg - name: Bryan Gin-ge Chen + github: bryangingechen descr: | Bryan is a senior engineer at the Mathlib Initiative. He did a PhD in theoretical condensed matter physics at University of @@ -62,6 +70,7 @@ img: bryan.jpg - name: Johan Commelin + github: jcommelin descr: | Johan is universitair docent (assistant professor) at Utrecht University (Netherlands) and the director of the Mathlib Initiative. @@ -70,6 +79,7 @@ img: Johan.jpg - name: Anatole Dedecker + github: ADedecker descr: | Anatole is a PhD student in Mathematics, specifically operator algebras, at Université Paris Cité (France). He has been formalizing @@ -77,6 +87,7 @@ img: anatole.jpg - name: Rémy Degenne + github: RemyDegenne descr: | Rémy is a researcher at the Inria centre at the University of Lille (France). He did a PhD in applied mathematics at Université Paris Cité. He has been @@ -84,6 +95,7 @@ img: remy.jpg - name: Floris van Doorn + github: fpvandoorn descr: | Floris is a professor in the mathematics department of the University of Bonn (Germany) on formal mathematics. @@ -93,6 +105,7 @@ img: floris.jpg - name: Frédéric Dupuis + github: dupuisf descr: | Frédéric is an Associate Professor of Computer Science at the Université de Montréal. His main area of research is quantum @@ -101,6 +114,7 @@ img: frederic.jpg - name: Gabriel Ebner + github: gebner descr: | Gabriel is an engineer at Microsoft Research (USA). He did a PhD in computational proof theory at TU Wien (Austria). @@ -110,6 +124,7 @@ img: gabriel.jpeg - name: Sébastien Gouëzel + github: sgouezel descr: | Sébastien is a Professor of Mathematics at Université de Rennes 1 (France). He did a PhD in dynamical systems in Orsay. He has @@ -117,14 +132,16 @@ now in Lean. img: sebastien.jpg - - name: Markus Himmel + name: Julia Markus Himmel + github: TwoFX descr: | - Markus is a tech lead at the Lean FRO. - He did a master's in pure mathematics in Cambridge (UK). - He has been formalizing mathematics since 2020. + Julia is a tech lead at the Lean FRO. + She did a master's in pure mathematics in Cambridge (UK). + She has been formalizing mathematics since 2020. img: markus.jpg - name: Simon Hudon + github: cipher1024 descr: | Simon is a research engineer and proof engineer at Bedrock Systems where he works on the formal verification of a novel hypervisor. He did a Master's @@ -136,12 +153,14 @@ img: Simon.jpg - name: Chris Hughes + github: ChrisHughes24 descr: | Chris is a PhD student at INRIA with the Gallinette team in Nantes (France). He has been formalizing mathematics since 2017. img: chris.png - name: Yury G. Kudryashov + github: urkud descr: | Yury is a Formalization Lead at Harmonic. He did a PhD in dynamical systems in Lyon and Moscow. @@ -149,6 +168,7 @@ img: yury.jpeg - name: Robert Y. Lewis + github: robertylewis descr: | Rob is a lecturer in the Department of Computer Science at Brown University (USA). @@ -158,6 +178,7 @@ img: rob.jpg - name: Jireh Loreaux + github: j-loreaux descr: | Jireh is an Associate Professor of Mathematics in the Department of Mathematics and Statistics at Southern Illinois University Edwardsville (USA). @@ -167,6 +188,7 @@ img: jireh.jpg - name: Marcelo Lynch + github: marcelolynch descr: | Marcelo is a senior engineer at the Mathlib Initiative, working on improving and maintaining ecosystem infrastructure. At previous positions, he has worked on @@ -174,6 +196,7 @@ img: marcelo.png - name: Heather Macbeth + github: hrmacbeth descr: | Heather is an Assistant Professor of Mathematics at Fordham University (USA). She did a PhD in differential geometry in Princeton. @@ -181,6 +204,7 @@ img: heather.jpeg - name: Patrick Massot + github: PatrickMassot descr: | Patrick is a Professor of Mathematics at Université Paris-Saclay at Orsay (France). He did a PhD in differential topology in @@ -188,12 +212,14 @@ img: patrick.png - name: Bhavik Mehta + github: b-mehta descr: | Bhavik is a PhD student in Mathematics at the University of Cambridge (UK). He has been formalizing mathematics since 2019. img: bhavik.jpg - name: Kyle Miller + github: kmill descr: | Kyle is a post-doc in mathematics at UC Santa Cruz and a research software engineer at the Lean FRO. @@ -202,6 +228,7 @@ img: kyle.jpg - name: Kim Morrison + github: kim-em descr: | Kim is a senior research engineer at the Lean Focused Research Organization. Their background is in mathematics, particularly topology and category theory. @@ -211,6 +238,7 @@ img: Kim.jpg - name: Oliver Nash + github: ocfnash descr: | Oliver is a mathematician who originally trained as a geometer. He is a senior manager at the Mathlib Initiative. He has @@ -222,15 +250,17 @@ img: ocfnash.png - name: Filippo A. E. Nuccio + github: faenuccio descr: | Filippo is an Associate Professor of Mathematics at Université Jean Monnet - in Saint-Étienne (France). He did a PhD in Algebraic Number Theory in Rome and + in Saint-Étienne (France). He did a PhD in Algebraic Number Theory in Rome and has been specialising in Iwasawa theory, alongside some archimedean and non-archimedean functional analysis. As an advocate for Open Science, he is a member of MathOA and of the French Committee for Open Science. He has been formalising mathematics since 2020. img: filippo.jpg - name: Joël Riou + github: joelriou descr: | Joël is an Associate Professor of Mathematics at Université Paris-Saclay at Orsay (France). He did a PhD in homotopy theory of schemes at @@ -238,12 +268,14 @@ img: joel.jpg - name: Michael Rothgang + github: grunweg descr: | Michael is a postdoc in the formalised mathematics group at the university of Bonn (Germany). He did a PhD in symplectic geometry at Humboldt-Universität zu Berlin. He has been formalising mathematics since 2023. - name: Damiano Testa + github: adomani descr: | Damiano is a reader in the Department of Mathematics at the University of Warwick (UK). He did a PhD in Algebraic Geometry at MIT (USA). @@ -251,6 +283,7 @@ img: damiano.jpeg - name: Adam Topaz + github: adamtopaz descr: | Adam is an Assistant Professor of Mathematics at the University of Alberta (Canada) and senior manager at the Mathlib Initiative. @@ -260,6 +293,7 @@ img: adam.jpg - name: Eric Wieser + github: eric-wieser descr: | Eric is a Senior Software Engineer on the AlphaProof team at Google DeepMind. He did a PhD formalizing Clifford algebras at the University of Cambridge (UK). @@ -268,6 +302,7 @@ img: eric.jpg - name: Leonardo de Moura + github: leodemoura descr: | Leo is a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS as well as Chief Architect and co-founder of the Lean FRO. @@ -277,14 +312,91 @@ img: leo.jpg - name: Wojciech Nawrocki + github: Vtec234 descr: | Wojciech is a PhD student at Carnegie Mellon University (USA). He has been contributing to open source software since 2016. img: wojciech.jpg - name: Sebastian Ullrich + github: Kha descr: | Sebastian is Head of Engineering and co-founder of the Lean FRO. He did a PhD on the Lean 4 frontend at Karlsruhe Institute of Technology (Germany). He has been working on Lean since 2015. img: sebastian.jpg +- + name: Aaron Anderson + github: awainverse +- + name: Alex J. Best + github: alexjbest +- + name: Andrew Yang + github: erdOne +- + name: Christian Merten + github: chrisflav +- + name: Dagur Asgeirsson + github: dagurtomas +- + name: David Loeffler + github: loefflerd +- + name: David Renshaw + github: dwrensha +- + name: Eric Rodriguez Boidi + github: ericrbg +- + name: Etienne Marion + github: EtienneC30 +- + name: Jon Eugster + github: joneugster +- + name: Joseph Myers + github: jsm28 +- + name: Jovan Gerbscheid + github: JovanGerb +- + name: Junyan Xu + github: alreadydone +- + name: Kexing Ying + github: kex-y +- + name: María Inés de Frutos-Fernández + github: mariainesdff +- + name: Michael Stoll + github: MichaelStollBayreuth +- + name: Miyahara Kō + github: Komyyy +- + name: Monica Omar + github: themathqueen +- + name: Moritz Doll + github: mcdoll +- + name: Robin Carlier + github: robin-carlier +- + name: Ruben Van de Velde + github: Ruben-VandeVelde +- + name: Thomas Browning + github: tb65536 +- + name: Thomas R. Murrills + github: thorimur +- + name: Yakov Pechersky + github: pechersky +- + name: Yaël Dillies + github: YaelDillies diff --git a/data/teams.yaml b/data/teams.yaml index d617688bca..90171c8b17 100644 --- a/data/teams.yaml +++ b/data/teams.yaml @@ -84,7 +84,7 @@ - Jon Eugster - Jovan Gerbscheid - Sébastien Gouëzel - - Markus Himmel + - Julia Markus Himmel - Simon Hudon - Yury G. Kudryashov - Robert Y. Lewis From 975e78fc0fa308e2c5de2a1799a5edf3fa0cd554 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Thu, 7 May 2026 14:57:44 -0400 Subject: [PATCH 4/5] Render reviewer free_form as markdown, show GitHub username inline Lets reviewers use links and emphasis in their interests blurb. Also puts the GitHub handle next to the name with inline styling instead of a block 
.

Co-Authored-By: Claude Opus 4.7 (1M context) 
---
 css/lean.css         | 3 +++
 scss/lean.scss       | 4 ++++
 templates/_team.html | 5 ++---
 3 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/css/lean.css b/css/lean.css
index 4dc17feb0e..21d9a0802b 100644
--- a/css/lean.css
+++ b/css/lean.css
@@ -8237,6 +8237,9 @@ pre {
 .card-body > *:first-child {
   margin-top: unset; }
 
+.reviewer-freeform > p:last-child {
+  margin-bottom: 0; }
+
 /* Theorem statements in the 100 theorem list: */
 .doc-stmt {
   font-family: 'Source Code Pro', monospace;
diff --git a/scss/lean.scss b/scss/lean.scss
index 924786a398..a299670cd3 100644
--- a/scss/lean.scss
+++ b/scss/lean.scss
@@ -120,6 +120,10 @@ pre {
   margin-top: unset;
 }
 
+.reviewer-freeform > p:last-child {
+  margin-bottom: 0;
+}
+
 /* Theorem statements in the 100 theorem list: */
 
 .doc-stmt {
diff --git a/templates/_team.html b/templates/_team.html
index 595abd787b..9f0d23fb9a 100644
--- a/templates/_team.html
+++ b/templates/_team.html
@@ -25,14 +25,14 @@ 
{{ member.name }}

         
    
         {% for member in team.members %}
           
  • 
-            {{- member.name -}}
+            {{- member.name }} (@{{ member.github }})
             {%- if reviewer_data is defined and member.github and member.github in reviewer_data -%}
               {%- set rd = reviewer_data[member.github] -%}
               {%- for label in rd.preferred_labels %}
                 {{ label }}
               {%- endfor %}
               {%- if rd.free_form %}
-                
    {{ rd.free_form }}
+                
    {{ rd.free_form | md }}
    
               {%- endif %}
             {%- endif %}
           
    • 
@@ -40,4 +40,3 @@ 
    {{ member.name }}
    
         

       {% endif %}
 {% endblock %}
-

From 005f5bad13d696383a7c357acb7aa69ae031d319 Mon Sep 17 00:00:00 2001
From: Bryan Gin-ge Chen 
Date: Sun, 10 May 2026 08:09:58 -0400
Subject: [PATCH 5/5] Apply suggestion from @bryangingechen

---
 templates/_team.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/templates/_team.html b/templates/_team.html
index 9f0d23fb9a..ca3b33ffba 100644
--- a/templates/_team.html
+++ b/templates/_team.html
@@ -25,7 +25,7 @@ 
{{ member.name }}

         
    
         {% for member in team.members %}
           
  • 
-            {{- member.name }} (@{{ member.github }})
+            {{- member.name }} (@{{ member.github }})
             {%- if reviewer_data is defined and member.github and member.github in reviewer_data -%}
               {%- set rd = reviewer_data[member.github] -%}
               {%- for label in rd.preferred_labels %}