Jesse Alama
@jessealama.net
Math and programming. Lean, JS, Racket. American. Igalian.
Reposted by Jesse Alama
There are many tools for unprivileged sandboxing on Linux. You should probably go use one of them. But I wrote shandbox to scratch my itch muxup.com/shandbox
/home/$user/sandbox shows up as /home/sandbox within the shared sandbox, which otherwise can only access explicitly mapped files/dirs.
/home/$user/sandbox shows up as /home/sandbox within the shared sandbox, which otherwise can only access explicitly mapped files/dirs.
shandbox
A simple shared sandbox using unshare+nsenter.
muxup.com
February 11, 2026 at 10:43 PM
There are many tools for unprivileged sandboxing on Linux. You should probably go use one of them. But I wrote shandbox to scratch my itch muxup.com/shandbox
/home/$user/sandbox shows up as /home/sandbox within the shared sandbox, which otherwise can only access explicitly mapped files/dirs.
/home/$user/sandbox shows up as /home/sandbox within the shared sandbox, which otherwise can only access explicitly mapped files/dirs.
Reposted by Jesse Alama
The program for Leaning In! 2026 is settled. We've got 11 (!) wonderful talks lined up. This is going to be a wonderufl time for digging into Lean,
Registration is open, but space is limited so if you're thinking of coming, please do register soon. See you in Berlin!
leaning.in/2026/
Registration is open, but space is limited so if you're thinking of coming, please do register soon. See you in Berlin!
leaning.in/2026/
Leaning In! 2026
A workshop for the Lean community - Thursday, March 12, 2026
leaning.in
February 12, 2026 at 12:26 PM
The program for Leaning In! 2026 is settled. We've got 11 (!) wonderful talks lined up. This is going to be a wonderufl time for digging into Lean,
Registration is open, but space is limited so if you're thinking of coming, please do register soon. See you in Berlin!
leaning.in/2026/
Registration is open, but space is limited so if you're thinking of coming, please do register soon. See you in Berlin!
leaning.in/2026/
Amazing work on an Erdős problem (whose original statement needed to be tweaked), demonstrating the power of AI-assisted proving in math. mathstodon.xyz/@tao/1158558...
Terence Tao (@tao@mathstodon.xyz)
Recently, the application of AI tools to Erdos problems passed a milestone: an Erdos problem (#728 https://www.erdosproblems.com/728) was solved more or less autonomously by AI (after some feedback…
mathstodon.xyz
January 19, 2026 at 1:58 PM
Amazing work on an Erdős problem (whose original statement needed to be tweaked), demonstrating the power of AI-assisted proving in math. mathstodon.xyz/@tao/1158558...
Lean Together 2026 starts today! It'll be four days of juicy Lean stuff. It's a remote-only conference, so feel free to join. See you there! leanprover-community.github.io/lt2026/
Home
A meeting all about Lean
leanprover-community.github.io
January 19, 2026 at 9:24 AM
Lean Together 2026 starts today! It'll be four days of juicy Lean stuff. It's a remote-only conference, so feel free to join. See you there! leanprover-community.github.io/lt2026/
Really alarming to see this story of "LLM psychosis".I first saw it in a video by Nate Jones. It looks like there's an attempt to solve the wildly difficult Navier-Stokes problem, backed up by a Lean formalization. youtu.be/AzOJ9QLgfIk
If This Can Happen to an Ex-DeepMind Leader, It Can Happen to You
My site: https://natebjones.com
Full Story w/ Self-Audit Framework:…
youtu.be
January 10, 2026 at 1:58 PM
Really alarming to see this story of "LLM psychosis".I first saw it in a video by Nate Jones. It looks like there's an attempt to solve the wildly difficult Navier-Stokes problem, backed up by a Lean formalization. youtu.be/AzOJ9QLgfIk
Claude Code helps me so much with the household chores. The dishes get washed more frequently, the apartment is appreciably tidier, the vacuum cleaner spends an above-average amount of time turned on, the trash gets taken out more quickly.
January 10, 2026 at 9:24 AM
Claude Code helps me so much with the household chores. The dishes get washed more frequently, the apartment is appreciably tidier, the vacuum cleaner spends an above-average amount of time turned on, the trash gets taken out more quickly.
💥 Breaking news from my Inbox 💥
I saved 251 hours on email with @SaneBox in 2025 #UnwrapYourInbox
See for yourself 👉 www.sanebox.com/unwrap/2pktu...
I saved 251 hours on email with @SaneBox in 2025 #UnwrapYourInbox
See for yourself 👉 www.sanebox.com/unwrap/2pktu...
Get rid of email clutter
Try SaneBox today and get 2 weeks for free!
www.sanebox.com
December 30, 2025 at 4:37 PM
💥 Breaking news from my Inbox 💥
I saved 251 hours on email with @SaneBox in 2025 #UnwrapYourInbox
See for yourself 👉 www.sanebox.com/unwrap/2pktu...
I saved 251 hours on email with @SaneBox in 2025 #UnwrapYourInbox
See for yourself 👉 www.sanebox.com/unwrap/2pktu...
TIL there's a JSON Schema validator for #lean at github.com/CAIMEOX/json... It seems to be abandoned, though (no activity for a year).
GitHub - CAIMEOX/json-schema-lean: Json Schema lean implementation
Json Schema lean implementation. Contribute to CAIMEOX/json-schema-lean development by creating an account on GitHub.
github.com
December 17, 2025 at 9:24 AM
TIL there's a JSON Schema validator for #lean at github.com/CAIMEOX/json... It seems to be abandoned, though (no activity for a year).
Enjoying the video from the December 2025 Mathlib community call.
Mathlib Community Meeting December 12, 2025
www.youtube.com
December 16, 2025 at 1:58 PM
Enjoying the video from the December 2025 Mathlib community call.
Reposted by Jesse Alama
We''ve landed a few more talks since the last update!
* Sorrachai Yingchareonthawornchai: The CSLib initiative
* Simon Sorg: Machine learning for Lean
* Jannis Limperg on Lean metaprogramming for AI
* Will Turner on the new ProofBench effort
Come join us for a day of #lean! leaning.in
* Sorrachai Yingchareonthawornchai: The CSLib initiative
* Simon Sorg: Machine learning for Lean
* Jannis Limperg on Lean metaprogramming for AI
* Will Turner on the new ProofBench effort
Come join us for a day of #lean! leaning.in
Leaning In! 2026
A workshop for the Lean community - Thursday, March 12, 2026
leaning.in
December 8, 2025 at 10:16 AM
We''ve landed a few more talks since the last update!
* Sorrachai Yingchareonthawornchai: The CSLib initiative
* Simon Sorg: Machine learning for Lean
* Jannis Limperg on Lean metaprogramming for AI
* Will Turner on the new ProofBench effort
Come join us for a day of #lean! leaning.in
* Sorrachai Yingchareonthawornchai: The CSLib initiative
* Simon Sorg: Machine learning for Lean
* Jannis Limperg on Lean metaprogramming for AI
* Will Turner on the new ProofBench effort
Come join us for a day of #lean! leaning.in
Incredible results with #lean and Gemini Deep Think by Tao in the Erdős Problem. It feels like a lot of doors in the formalization space, whether that's math or hardware/software verification, are opening quickly. mathstodon.xyz/@tao/1155914...
Terence Tao (@tao@mathstodon.xyz)
Over at the Erdos problem website, AI assistance is now becoming routine. Here is what happened recently regarding Erdos problem #367 https://www.erdosproblems.com/367 : 1. On Nov 20, Wouter van…
mathstodon.xyz
November 26, 2025 at 1:58 PM
Incredible results with #lean and Gemini Deep Think by Tao in the Erdős Problem. It feels like a lot of doors in the formalization space, whether that's math or hardware/software verification, are opening quickly. mathstodon.xyz/@tao/1155914...
The 2026 edition of the ITP (Interactive Theorem Proving) conference back in October featured a #lean event. It was great to be there and connect with so many Lean folks. The videos are finally available: www.youtube.com/playlist?lis...
ITP 2025 Lean Workshop
Share your videos with friends, family, and the world
www.youtube.com
November 14, 2025 at 9:24 AM
The 2026 edition of the ITP (Interactive Theorem Proving) conference back in October featured a #lean event. It was great to be there and connect with so many Lean folks. The videos are finally available: www.youtube.com/playlist?lis...
Reposted by Jesse Alama
Leaning In! 2026 is ON!
If you like #lean and are in Berlin, Germany, Europe, or anywhere on Earth, you are invited.
We've got a room at Spielfeld in Berlin. See you on March 12th!
More information, including tickets and the CfP, here: leaning.in/2026/
If you like #lean and are in Berlin, Germany, Europe, or anywhere on Earth, you are invited.
We've got a room at Spielfeld in Berlin. See you on March 12th!
More information, including tickets and the CfP, here: leaning.in/2026/
Leaning In! 2026
Leaning In! is a one-day workshop dedicated to the Lean programming language and proof assistant.
leaning.in
October 26, 2025 at 7:54 PM
Leaning In! 2026 is ON!
If you like #lean and are in Berlin, Germany, Europe, or anywhere on Earth, you are invited.
We've got a room at Spielfeld in Berlin. See you on March 12th!
More information, including tickets and the CfP, here: leaning.in/2026/
If you like #lean and are in Berlin, Germany, Europe, or anywhere on Earth, you are invited.
We've got a room at Spielfeld in Berlin. See you on March 12th!
More information, including tickets and the CfP, here: leaning.in/2026/
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
October 11, 2025 at 8:24 AM
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...
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
October 9, 2025 at 2:31 PM
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.
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
October 5, 2025 at 12:58 PM
TIL In Lean you can output the axioms that a proof depends on using a simple `#print axioms` command.
Reposted by Jesse Alama
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
September 3, 2025 at 1:41 PM
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...
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
October 5, 2025 at 8:24 AM
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.
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
October 4, 2025 at 12:58 PM
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.
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
October 4, 2025 at 8:24 AM
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.
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
October 3, 2025 at 12:58 PM
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.
Reposted by Jesse Alama
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
October 3, 2025 at 9:55 AM
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
Reposted by Jesse Alama
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...
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
October 2, 2025 at 1:16 PM
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...
2026.splashcon.org/track/oopsla...
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
October 2, 2025 at 12:58 PM
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!
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!
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
September 22, 2025 at 1:50 PM
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!
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!