Lightnews — Scholar-powered news

xenaproject.bsky.social @xenaproject.bsky.social · 4d

Good question. They're available on my hard drive but Simons never asked for them. I've uploaded them to the Lean Zulip here leanprover.zulipchat.com#narrow/chann...

Public view of Lean | Zulip team chat

Browse the publicly accessible channels in Lean without logging in.

leanprover.zulipchat.com

2

xenaproject.bsky.social @xenaproject.bsky.social · 5d

My talk at the Simons Foundation last week is now up on YouTube youtube.com/watch?v=K5w7VS2sxD0 . It is a hopefully-comprehensible general audience talk about what I think is a big decision which mathematicians will have to decide whether to back or not.

Kevin Buzzard - Where is Mathematics Going? (September 24, 2025)

YouTube video by Simons Foundation

youtube.com

1 3 11

xenaproject.bsky.social @xenaproject.bsky.social · 11d

My colleague Jon Mestel pointed out to me that whether you use the US 09272025 date system or the pretty-much-everywhere-else-in-the-world-and-far-saner 27092025 system, today's date is a perfect square, as is the current month and the year! Will this ever happen again??

8

xenaproject.bsky.social @xenaproject.bsky.social · 20d

Of course Barbara! Thanks for asking!

1

xenaproject.bsky.social @xenaproject.bsky.social · 20d

Amongst the projects funded is my project www.renaissancephilanthropy.org/a-dataset-of... to create what in 2025 is a super-hard dataset of pairs (informal hard proof, formal statement) of recent results from top journals. The challenge for machine is to formalise the rest of the paper.

www.renaissancephilanthropy.org

1 2 10

xenaproject.bsky.social @xenaproject.bsky.social · 20d

Renaissance Philanthropy have announced the first 29 grants they've given from their AI For Math fund www.renaissancephilanthropy.org/ai-for-math-... . Interesting to see that around half of the funded proposals mention Lean.

AI for Math Winners Page — Renaissance Philanthropy – A brighter future for all through science, technology, and innovation

www.renaissancephilanthropy.org

1 1 15

xenaproject.bsky.social @xenaproject.bsky.social · Aug 22

The Mathlib Initative is hiring! www.renaissancephilanthropy.org/careers/math... (part-time contractor, helping to solve the "2000 PRs" issue, note the required qualifications) and www.renaissancephilanthropy.org/careers/devo... (full-time, solving distributed systems challenges). 14 Sept deadline.

Mathematical Research Engineer — Renaissance Philanthropy – A brighter future for all through science, technology, and innovation

www.renaissancephilanthropy.org

1 7 16

xenaproject.bsky.social @xenaproject.bsky.social · Aug 12

Mathematics is also incomplete (assuming it's consistent) and that hasn't stopped lean from engaging with it at research level

2

Reposted

emilyriehl.bsky.social @emilyriehl.bsky.social · Aug 7

@sciam.bsky.social gave me the opportunity to share some personal thoughts about the recently reported AI results from the #imo2025:

www.scientificamerican.com/article/math...

AI Crushed the Math Olympiad—Or Did It?

AI models supposedly did well on International Math Olympiad problems, but how they got their answers reminds us why we still need people doing math

www.scientificamerican.com

6 9

xenaproject.bsky.social @xenaproject.bsky.social · Aug 6

Could you ever envisage lean being useful to verify nontrivial code written in common programming languages or is this asking too much?

2 2

xenaproject.bsky.social @xenaproject.bsky.social · Aug 4

I absolutely agree; IPAM is the notable absentee from the list. I organised a conference there in 2023 www.ipam.ucla.edu/programs/wor... bringing together people from mathematics and machine learning and formal methods, and it was a fascinating week!

5

xenaproject.bsky.social @xenaproject.bsky.social · Aug 4

NSF announces funding for ICARM: the Institute for Computer-Aided Reasoning in Mathematics, based in Carnegie-Mellon . Amazing! Carnegie-Mellon press release here: www.cmu.edu/news/stories...

www.nsf.gov/news/nsf-inv...

NSF invests over $74 million in 6 mathematical sciences research institutes

The U.S. National Science Foundation is investing over $74 million in six research institutes focused on the mathematical sciences and their broad applications in all fields of science, technology and...

www.nsf.gov

1 7 16

xenaproject.bsky.social @xenaproject.bsky.social · Aug 3

Lol that was me a few years ago

1

xenaproject.bsky.social @xenaproject.bsky.social · Aug 3

Sunday afternoon.

A level from the computer game "Baba is you"

1 10

xenaproject.bsky.social @xenaproject.bsky.social · Aug 3

Thoughts on AI and the IMO.

xenaproject.wordpress.com/2025/08/03/a...

AI at IMO 2025: a round-up

Setting the scene The 2025 International Mathematics Olympiad has come and gone. Reminder: this is an exam for high-school kids across the world (each country typically sends six kids), comprising …

xenaproject.wordpress.com

1 7 24

xenaproject.bsky.social @xenaproject.bsky.social · Jul 31

I did read parts of Langlands document about defining local epsilon factors locally and it was just page after page of representation theory (so it looked like groups acting on vector spaces)

4

xenaproject.bsky.social @xenaproject.bsky.social · Jul 31

I have never read the algebraic proof of the first inequality in global class field theory, I've just heard that it exists. I read the analytic proof last week though :-) The elementary proof of the prime number theorem still has plenty of basic real analysis in it.

2

xenaproject.bsky.social @xenaproject.bsky.social · Jul 31

Featuring a sorry-free proof that 2+2=6

dan @danabra.mov · Jul 30

⚛️📝 New on Overreacted: The Math Is Haunted

The Math Is Haunted — overreacted

A taste of Lean.

overreacted.io

14

xenaproject.bsky.social @xenaproject.bsky.social · Jul 30

The construction of local epsilon factors in the Langlands program was done by Langlands in an unpublished document which is hundreds of pages long. Then Deligne discovered a global construction which uses L-functions at some point and which fits into 30 pages

3

xenaproject.bsky.social @xenaproject.bsky.social · Jul 30

The fact that there exists a class formation for global fields (this is a higher reciprocity statement in number theory) boils down to proving two inequalities and traditionally one of them was done analytically (using L-functions like PNT) but now purely algebraic proofs are known.

2 4

xenaproject.bsky.social @xenaproject.bsky.social · Jul 28

Thanks for asking Barbara. The salary range is £48,056 - £56,345 per annum. I made some enquiries and the visa question is infinitely more complicated because there are a gazillion different kinds of visas depending on the applicant. The price could range from hundreds to thousands.

1 4

xenaproject.bsky.social @xenaproject.bsky.social · Jul 28

Why is this a worthwhile project?

1) It will create a hard dataset for autoformalization AI's;

2) It will force us to formalize the definitions of mathematical objects which are being used today in the top journals, thus making Lean's mathematics library more relevant to modern math researchers.

xenaproject.bsky.social @xenaproject.bsky.social · Jul 28

I am advertising for 4 post-docs to come to Imperial and formalize, in Lean, *statements* of theorems from recent issues of the top generalist pure mathematics journals.

www.imperial.ac.uk/jobs/search-...

Positions are for 2 years, start date 1st Oct this year. Deadline 15th August.

Description

Please note that job descriptions are not exhaustive, and you may be asked to take on additional duties that align with the key responsibilities ment...

www.imperial.ac.uk

10

xenaproject.bsky.social @xenaproject.bsky.social · Jul 28

I am advertising for 4 post-docs to come to Imperial and formalize, in Lean, *statements* of theorems from recent issues of the top generalist pure mathematics journals.

www.imperial.ac.uk/jobs/search-...

Positions are for 2 years, start date 1st Oct this year. Deadline 15th August.

Description

Please note that job descriptions are not exhaustive, and you may be asked to take on additional duties that align with the key responsibilities ment...

www.imperial.ac.uk

2 13 29

xenaproject.bsky.social @xenaproject.bsky.social · Jul 24

A new "Mathlib initiative" focussed around Lean's mathematics library has been announced. Thanks to the generosity of Alex Gerko and XTX Markets, there is finally an official entity focussed on growing this 21st century way of doing mathematics.

www.renaissancephilanthropy.org/news-and-ins...

Lean FRO and Mathlib receive $10M from XTX Markets Founder Alex Gerko to further advance the use of AI for mathematical research — Renaissance Philanthropy – A brighter future for all through science,...

FOR IMMEDIATE RELEASE July 24, 2025 Contact: [email protected] ; [email protected] ; [email protected]

www.renaissancephilanthropy.org

4 21

xenaproject.bsky.social @xenaproject.bsky.social · Jul 19

Note that no official IMO markers were involved in the marking of the solutions. I am also unclear about whether many solutions were generated and then humans chose the ones most likely to be correct, or whether the machine gave one "final answer" to each question with no human intervention.

1 1 11