Lightnews — Scholar-powered news

Jesse Alama @jessealama.net · 5d

Fascinating talk by Kevin Buzzard about where he sees math going, why it has a big problem (for some time now, even predating the internet), and why #lean might be part of the solution. hackaday.com/2025/10/08/w...

Where Is Mathematics Going? Large Language Models And Lean Proof Assistant

If you’re a hacker you may well have a passing interest in math, and if you have an interest in math you might like to hear about the direction of mathematical research. In a talk on this top…

hackaday.com

1

Jesse Alama @jessealama.net · 7d

Really excited to see the #lean Mathlib Initiative take off. Here’s their new web page. Mathlib is such a huge, and growing, project; this help from Renaissance Philanthropy is very welcome.

The Mathlib Initiative

The Mathlib Initiative supports the development of mathematical libraries in the Lean theorem prover.

mathlib-initiative.org

Jesse Alama @jessealama.net · 11d

TIL In Lean you can output the axioms that a proof depends on using a simple `#print axioms` command.

Axioms

Axioms are postulated constants. While the axiom's type must itself be a type (that is, it must have type Sort u), there are no further requirements. Axioms do not reduce to other terms.

lean-lang.org

Reposted by Jesse Alama

Paulo Matos @p.ocmatos.com · Sep 3

Even if you didn't have the chance to listen to any of the amazing Igalia Chats - it's time for you to start with a really good chat about #Webassembly, with the one and only @wingolog.org . open.spotify.com/episode/0DmQ...

Wingo on Wasm

open.spotify.com

1 2 9

Jesse Alama @jessealama.net · 11d

I was reminded of the Blueprint tool for sketching mathematical profs in Lean. I haven’t used it yet but I’m going to see if this can help me structure my work. Also curious to see how Blueprint applies in other scenarios such as software verification.

GitHub - PatrickMassot/leanblueprint: plasTeX plugin to build formalization blueprints.

plasTeX plugin to build formalization blueprints. Contribute to PatrickMassot/leanblueprint development by creating an account on GitHub.

github.com

1

Jesse Alama @jessealama.net · 12d

Some reflections by Terence Tao on different levels, of formalization and rigor in math. This was offered as a discussion topic in the afternoon session of the Lean workshop at ITP 2026 but we didn’t really get around to it.

There’s more to mathematics than rigour and proofs

The history of every major galactic civilization tends to pass through three distinct and recognizable phases, those of Survival, Inquiry and Sophistication, otherwise known as the How, Why, and Wh…

terrytao.wordpress.com

1 1

Jesse Alama @jessealama.net · 12d

This is a real eye-opening article where @ghuntley.com builds a compiler for a new language using LLVM and the amazing technique he calls Ralph Wiggum.

Ralph Wiggum as a "software engineer"

😎Here's a cool little field report from a Y Combinator hackathon event where they put Ralph Wiggum to the test. "We Put a Coding Agent in a While Loop and It Shipped 6 Repos Overnight"…

ghuntley.com

Jesse Alama @jessealama.net · 13d

I haven’t yet dived in to git worktrees but as I continue to learn and reflect more on AI-assisted working, I realize this is pretty much the feature i need. This article made things click.

Claude Code - AI Pair Programming Assistant | ClaudeCode.io

Transform your development workflow with Claude Code, the most advanced AI coding assistant powered by Claude Opus 4.1 and Claude Sonnet 4.5.

ClaudeCode.io

Jesse Alama @jessealama.net · 13d

Fantastic article. I love the idea of embracing Ralph, letting him screw up but encouraging him to learn. I’m going to try applying Ralph to some of my projects. Thanks!

Reposted by Jesse Alama

Nordic.js @nordicjs.com · 13d

No more juggling CommonJS and faux-ESM. @joyeecheung.bsky.social revealed how Node.js is moving to full ESM and why the future looks brighter for developers. #NordicJS #NordicJS2025

2 11

Reposted by Jesse Alama

Shriram Krishnamurthi @shriram.bsky.social · 14d

OOPSLA 2026 deadline is just a week away! Can you please help us get the word out by sharing? Thanks!
2026.splashcon.org/track/oopsla...

SPLASH 2026 - OOPSLA - SPLASH 2026

Welcome to the website of the SPLASH 2026 conference. We are working hard to fill the website with all related information. Please check back soon! In the meantime, please consider this overview of th...

2026.splashcon.org

1 23 19

Jesse Alama @jessealama.net · 14d

Just arrived in Reykjavik for the #lean workshop as part of ITP 2025 leanprover-community.github.io/itp-2025-lea... I'll be presenting some of my recent work. Looking forwrard to (re)connecting with some fellow Leaners!

Home

Lean Workshop at Interactive Theorem Proving 2025 - 2 October 2025, Reykjavik, Iceland

leanprover-community.github.io

2 3

Jesse Alama @jessealama.net · 24d

TIL pre-commit.com

I was just browsing the #lean Mathlib repo toplevel directory and noticed a file with an unusual, but suggestive name. Took a look inside and...love it!

pre-commit

A framework for managing and maintaining multi-language pre-commit hooks.

pre-commit.com

Jesse Alama @jessealama.net · Sep 14

I was greatly assisted by Claude Code and LeanSerch (leansearch.net).

Mathlib4 Search

Find theorems in Mathlib4 using natural language query

leansearch.net

Jesse Alama @jessealama.net · Sep 14

I'm happy to announce that I've finally wrapped up a proof of Euler's polyhedron formula ("V - E + F = 2") and submitted a PR to Mathlib. I've been working on this in bits and pieces on evenings and weekends.

github.com/leanprover-c...

feat: Euler's polyhedron formula via homological algebra by jessealama · Pull Request #29639 · leanprover-community/mathlib4

Summary This PR adds a proof of Euler's polyhedron formula (V - E + F = 2) using homological algebra, completing theorem #13 from Freek Wiedijk's list of 100 theorems. Mathematical Overview...

github.com

1

Jesse Alama @jessealama.net · Aug 26

TFW you start to realize you're not going to win the game of type tetris.

Jesse Alama @jessealama.net · Aug 26

The Kimina theorem prover at Project Numina is an amazing piece of technology. This kind of targeted, special-purpose LLMs seems to be just what is needed. They don't even need to be large; "small" LLMs might be just fine. demo.projectnumina.ai

Kimina Prover Demo – AI-Powered Proof Validation in Action

Try the live demo of Kimina Prover – a new AI-powered assistant for interactive proof validation. Test it now!

demo.projectnumina.ai

Jesse Alama @jessealama.net · Aug 23

Brilliant. Hope there’s a bit of joy mixed in the visits, too.

1 1

Jesse Alama @jessealama.net · Aug 23

Just had my first success using the new grind tactic in a #lean proof. I didn't know it was even going to work; I was stuck and reached for it only as a hail-mary desparation move. It worked! Mind blown.

2

Jesse Alama @jessealama.net · Aug 22

Happy to announce a new polyfill for the in-progress Ecma TC39 amount proposal! The proposal all about mathematical values together (optionally) with a unit and a precision (understood either as significant or fractional digitis)

proposal-amount

Polyfill for TC39 Amount proposal. Latest version: 20250821.0.0, last published: 7 minutes ago. Start using proposal-amount in your project by running `npm i proposal-amount`. There are no other…

www.npmjs.com

1 2

Jesse Alama @jessealama.net · Aug 22

Huge congratulations in order for the #lean Mathlib team for securing a generous donation to help keep things going and improve things further there. Really looking forward to seeing the next steps here. 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, technology, and innovation

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

www.renaissancephilanthropy.org

1

Jesse Alama @jessealama.net · Aug 21

Congratulations to the #lean team on the 4.22 release! This is an exciting one for me for two reasons: the new grind tactic and new support for verification of imperative programs using Hoare triples. lean-lang.org/doc/referenc...

Lean 4.22.0 (2025-08-14)

For this release, 468 changes landed. In addition to the 185 feature additions and 85 fixes listed below there were 15 refactoring changes, 5 documentation improvements, 4 performance improvements, 0…

lean-lang.org

Jesse Alama @jessealama.net · Aug 21

Delighted to see the new Institute for Computer-Aided Reasoning in Mathematics. With many overlapping and fellow-travelling communities in academia, industry, even citizen science, a new institute of this kind is probably what we need right now. www.cmu.edu/news/stories...

New NSF Institute at CMU Will Help Mathematicians Harness AI and Advance Discoveries

The Institute for Computer-Aided Reasoning in Mathematics (ICARM) — one of just six mathematics institutes across the U.S. to receive NSF support — will help researchers modernize mathematical…

www.cmu.edu

2

Jesse Alama @jessealama.net · Aug 20

Topics discussed included: the upcoming (funded) Mathlib initiative, the new grind tactic and how to think about it, whether we should be using type classes to pack in arbitrary background knowledge (and how such an approach might rope in unnecessary background knowledge or otherwise be unwelcome).

Jesse Alama @jessealama.net · Aug 20

The August 2025 Mathlib community call was really great to watch. Thanks for putting it on YouTube. youtu.be/dUWiG12ZQ4g

Mathlib Community Meeting August 8, 2025

youtu.be

1 1