Tessera
Folgen

@xenaproject.bsky.social

121 Posts811 Follower26 Folgt
@xenaproject.bsky.social · 9mo ago

It's funny how mathematicians sometimes confuse 0 and infinity. We say that the characteristic of a field can be 0, but that the order of an element in a group can be infinity. These are two different conventions expressing the same idea. 1/2

@xenaproject.bsky.social · 9mo ago

Here's the statement in Lean. How little can one get away with importing in order to prove this? Can it be proved by induction on max(l)-min(l) for example, avoiding the reals completely?

If L is a list of naturals, then its length to the power of its length, multiplied by its product, is at most its sum to the power of its length.
@xenaproject.bsky.social · 9mo ago

Fermat's Last Theorem is a famous example of a question which can be stated using only naturals and whose proof requires a lot of machinery. But in fact the AM-GM inequality, just for ℕ, can be stated purely using ℕ (clear denoms, raise everything to n'th power). Is there a simple proof avoiding ℝ?

@xenaproject.bsky.social · 9mo ago

Fermat's Last Theorem is a famous example of a question which can be stated using only naturals and whose proof requires a lot of machinery. But in fact the AM-GM inequality, just for ℕ, can be stated purely using ℕ (clear denoms, raise everything to n'th power). Is there a simple proof avoiding ℝ?

@xenaproject.bsky.social · 10mo ago

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??

@xenaproject.bsky.social · last yr.

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...

nsf.gov

@xenaproject.bsky.social · last yr.

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 · last yr.

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.

@xenaproject.bsky.social · last yr.

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...

imperial.ac.uk

@xenaproject.bsky.social · last yr.

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: media@renphil.org ; richard.hillary@xtxmarkets.com ; pr@convergentresearch.org

renaissancephilanthropy.org

@xenaproject.bsky.social · last yr.

Terry Tao has translated his "Analysis I" textbook into Lean! github.com/teorth/analy... Projects like this are tough to pull off, and need users to play through the levels and find and eliminate things which the formalization is making artificially hard. Fork the repo and give the exercises a try!

GitHub - teorth/analysis: A Lean companion to Analysis I

A Lean companion to Analysis I. Contribute to teorth/analysis development by creating an account on GitHub.

github.com

@xenaproject.bsky.social · last yr.

I have a gig in Southampton next week! www.turnersims.co.uk/whats-on/mat... Thurs 19th June 2025, 4pm, tickets are free but need to be booked in advance, I'll be explaining what I learnt this week in Cambridge about where we are with AI and mathematics, and summarising for a general audience.

Mathematics and AI: Generating the Future How will AI change mathematics? - Turner Sims

There’s no shortage of headlines proclaiming that AI will soon revolutionise everything — including mathematics — and leave no profession untouched. But what’s really happening behind the scenes? In t...

turnersims.co.uk

@xenaproject.bsky.social · last yr.

I'm at Big Proof this week. Bhavik Mehta's talk (video not yet up) contained a big surprise at the end: one of the references in a paper he's formalizing is an old 4-page paper about bounds for the ABC conjecture, and the paper has been completely *autoformalized* by Morph Labs' AI model "Trinity".