CS PhD student @DrexelCCI working on formalization in Lean. Maintainer of cslib.io/. Student Researcher @GoogleDeepMind
Joined December 2014
- Tweets 4,762
- Following 2,682
- Followers 1,019
- Likes 12,796
217 Photos and videos
Pinned Tweet
17 Sep 2021
I figured my math followers would especially appreciate this! Just got these, they are originals from 1740 and 1751. Include the original publication of Euler's solution to the Basel problem, among other very cool things. So crazy to have these pieces of history on my bookshelf.
3
5
51
Jun 9
An interesting read. (As I've come to always expect from Shriram!)
I've spent months rethinking and rebuilding my programming languages course from scratch for the agentic coding era. I wrote myself a memo explaining what I'm doing. I figure others might be interested in the redesign, so here goes! Feedback welcome ofc.
docs.google.com/document/d/e…
3
168
Jun 3
The other half missed in these conversations is that formalization is also a human endeavor! Probably the most important factor that has centered Lean for AI usage is the social convergence of a unified Mathlib, which is only possible with a huge amount of human interaction
Mathematics -is- a human endeavour.
There is something which maybe you're calling mathematics that has nothing to do with humans, some 'platonic otherworld' of abstract ideas. But what I call mathematics is the human attempt to explore and understand this world.
1
8
575
Jun 2
I signed this as well. Minus some minor quibbles about how formalization is framed, I agree with the points it makes.
I have signed the Leiden declaration, and encourage everyone to read it and reflect.
Even if some of the points are impossible to achieve in reality, they are a good set of guidelines to try and do what is best for humanity.
leidendeclaration.ai/
2
173
Chris Henson retweeted
May 20
You can read my thoughts and those of some others here. In particular I strongly recommend reading what Thomas Bloom and Melanie Matchett Wood have to say about it: cdn.openai.com/pdf/74c24085-…
7
19
194
22,599
Apr 29
A ship without a captain, taking all the world's software along for the voyage
Apr 28
People who are sharing their take about reliability at GH:
- The COO (owning operations)
- The CTO (engineering)
- The CPO (product)
They are all peers to one another, and a subset of GH staff reports to them.
You know who we don't hear from? The CEO. Because there is none.
1
203
Apr 25
Just to clarify, this is very much WIP documentation about Lean's newest proof automation. I am not a developer for core Lean. I put it somewhere public to encourage discussion on Zulip; these are not "official" docs yet. (But I think it's pretty uncontroversial advice!)
Apr 24
grind best practices. ~ Chris Henson. github.com/chenson2018/leanp… #LeanProver
1
2
400
Apr 23
It's great to promote a variety of proof assistants and compare technical differences. Given the title though, it's essential to discuss controversial trade-offs in Lean like definitional proof irrelevance and liberal elaboration. Without this thorough comparison seems difficult.
Apr 23
New on my blog: "Why not use Lean?"
lawrencecpaulson.github.io/2…
2
1
10
688
Apr 14
For those interested in this conversation, this Zulip thread is at: leanprover.zulipchat.com/#na…
1
7
408
Chris Henson retweeted
Slightly unfortunate that this article fails to acknowledge (a) the 2 years of hard work that preceded the Gauss formalisation (b) the fact that the project is not finished. It’s also unclear what “verified” means when they say “the proofs had already been verified without AI.”
Apr 11
The Economist on AI, math, formalization.
Includes a choice quote from me and thoughts from @TerrenceTao, @pushmeet, @tachim @HarmonicMath, @wtgowers, Don Knuth & Filip Stappers, and mention of @mathematics_inc and Maryna Viazovska
economist.com/science-and-te…
1
16
88
12,245
Apr 9
My own take:
1
6
545
Mar 21
> Programming languages, a domain that does not have deep established cultural history
*sigh*
Mar 21
Programming languages, a domain that does not have deep established cultural history, quickly adopted syntax formatting and highlighting, because those things are better for readability.
Math notation has a much deeper cultural history, and also did a similar thing: math notation is inherently a very 2D language, because that's better for readability.
I think it's reasonable to believe that the underlying advantages of these styles are likely also at least sometimes true for written text.
Prose is one-dimensional because we historically have such a strong tradition of wanting spoken text and written text to correspond to each other. Now, we get an opportunity to re-evaluate that convention, and we discover that patterns other than one-dimensional linear prose are more reader-friendly, of which bullet points are a major one.
I think this is all a healthy development.
16
21
879
46,437
Mar 17
It's interesting how we now have domain specific AI tells. When someone opens with "no axioms, zero sorry" about a Lean proof, it is almost guaranteed to be AI-generated.
7
321
Mar 5
Your regularly scheduled Lean posting is now on pause while I am busy Slaying the Spire (2)
The Spire has finally reawakened. ⚔️
Slay the Spire 2 is out now in Steam Early Access!!
New characters, enemies, environments, a co-op mode & more await you in this sequel to the iconic roguelike deckbuilder. Join the journey now to be a part of the Spire's next evolution!
5
194
Mar 4
I'm probably about a million years late to this, but `gh checkout pr` is so nice to use. Never again am I going to waste mental effort remembering what to do when someone makes a PR from the main branch of their fork.
1
147
Mar 3
Wow, what a fun and specialized promotion. I am just as impressed with the technical section of the bookstore having its own account!
【フェア開催中！】
現在、この動画で選書いただいた書籍にて、「世界圏論化計画」と題しフェアを開催しております。
数学書や人文書から数学、圏論にアプローチする書籍を多数お選びいただきました。ご推薦書籍にコメントを掲示。直筆POPもぜひご覧ください！
19番フェア棚にて。
#世界圏論化計画
1
203
Mar 3
For anyone wondering how to trust the sphere packing proofs from Gauss. This, the most paranoid checking that treats the binary serialization of proofs as potentially malicious plus Mathlib contributors checking definitions is as much assurance as can be asked for in my opinion.
15
1,075
Chris Henson retweeted
We had a few cryptography in Lean related talks in the last few weeks ahead of ArkLib being presented at RWC later this month:
1
4
20
1,984
Chris Henson retweeted
Feb 27
🚨 Putting this back on your radar:
The deadline for the ICERM Graduate Training Workshop on ∞-categories with proof-assistants (organized with @emilyriehl and Jonathan Weinberger) is getting close!
📬Application deadline: March 31, 2026.
Full details in the post below 👇
7 Nov 2025
🌞Summer School Announcement🌞
🎓∞-Category Theory at @ICERM !🎓
I am happy to announce that together with @emilyriehl & Jonathan Weinberger we are organizing a Graduate Training Workshop teaching ∞-category theory via proof assistants!🧠💻
More infos in the next post👉
1
2
15
2,055
Feb 27
Anime meme spam in the Lean Zulip, does this mean we're mainstream now???
1
167
Feb 23
An interesting angle that lines up with some of my intuitions:
- the influence of Mathlib on Lean benchmarks
- qualitative differences between CS/math that affect AI formalization
I hope in the future this can consider CSLib, which occupies an interesting space wrt these points.
Introducing VeriSoftBench — a benchmark for repository-scale Lean 4 verification proofs!
📦 500 proof obligations from 23 open-source formal-methods repos
🧩 Preserves real repo context cross-file dependencies
🧪 Two eval modes: Curated deps vs Full repo context
📉 Frontier LLMs still struggle: best achieves 41.0% (curated) / 34.8% (full repo)
1
7
550