Hacker Newsnew | past | comments | ask | show | jobs | submitlogin
AxEy18 hours ago | parent | context | favorite | on: Lean now ships with verified kernels > Suppose lean in its current state existed 15 years ago, and suppose the math community eagerly started contributing en masse to a shared repository of code. How much of the breakthroughs and longstanding questions in mathematics that we’ve seen answered this year do you think we would have solved? (Former grad student in math here who has spent whole weeks formalizing in Lean lemmas that would be considered by professional mathematicians writing a mathematics text / paper as obvious ("without loss of generality we can assume that....", "it should be clear that...") Probably very few or none. These systems (mostly) don't help you discover new mathematics. They are a tool for formalization. It just turns out that combining them with LLMs is the secret sauce. LLMs have quite a bit of creativity but make a lot of mistakes. The Lean typechecker never makes a mistake but has no creativity. Get them to work together in an iterative loop and you get what we have now. help 
xiaoyu200618 hours ago | next[–] I am a math undergrad and I tried lean. It probably is because of habit and familiarity but I still find lean proofs harder to read than NL proofs. I wonder what if the math education switch entirely to a formal language (not necessarily Lean) will be? reply fspeech5 hours ago | parent | next[–] Ask a model (dsv4.1 flash works great on this) to explain the proof to you so you can get an idea of the overall concept and structure first. Formalized math tends to encode math a certain way to make it easier for Lean, which doesn't have a visual cortex, but harder for people. reply dnautics5 hours ago | parent | prev | next[–] As a former math major (and developer) it bugged me that lean is optimized for WRITING proofs and not for READING proofs. I'm noodling around with a language that is optimized for reading proofs: https://github.com/ityonemo/2b4m The tradeoff is that it's more verbose, but you don't have to even know the language to properly decode a proof. as an exercise for the language, I'm playing around with having Claude formalize an online algebra text: https://github.com/ityonemo/2b4m/tree/main/aata LMK what you think reply thejokeisonme2 hours ago | root | parent | next[–] Putting aside the Claudisms. You only compare to tactic heavy languages, which is what you don't like about them. Try looking at Agda, Idris, Mikan,... They work with pattern matching not just for definitions but for proofs as well, so the derivation is laid bear. Not saying your niche doesn't have value, but you can get interesting ideas from there. reply dnautics1 hour ago | root | parent | next[–] Thanks, good advice! Aside: To some degree, the claudisms are the point since the PL is written by Claude and intended to be consumed by claude reply curt159 hours ago | parent | prev | next[–] "Mathematics is commonly explained and recorded in symbolic and concrete forms that are easy to communicate, rather than in conceptual forms that are easy to understand once communicated. Translation in the direction conceptual -> concrete and symbolic is much easier than translation in the reverse direction, and symbolic forms often replaces the conceptual forms of understanding." https://mathoverflow.net/questions/43690/whats-a-mathematici... reply asa12316 hours ago | parent | prev | next[–] i feel like this would be the equivalent of having all CS undergrads program with assembly and assembly only. it might(?) work? but abstractions exist for a reason (mostly...) reply xiaoyu200616 hours ago | root | parent | next[–] It's completely different things. Math itself is abstraction. Lean is formalized abstraction that don't let you write "it is immediately obvious that" reply tux313 hours ago | root | parent | next[–] Lean tactics can handle obvious things automatically, for some value of "obvious". reply dnautics5 hours ago | root | parent | next[–] I think this is kinda the problem with lean, to be frank. Sometimes it's not obvious what lean is doing. (unless you're interactive) reply markburns13 hours ago | root | parent | prev | next[–] Knowing very little about lean but speculating here: is lean something that could output a few natural language expressions at key points so that you can still have “it should be clear that” for the natural language reader but have it undeniably proven. Ie entrust the more tedious aspects but be able to follow along and still have references to check if you are curious about thoroughness. Almost like a tap with a latex renderer at various insertion points? reply black_knight12 hours ago | root | parent | prev | next[–] I have hear people make this comparison many times, but it just does not hold up under scrutiny. I think the confusion stems from people being exposed to set theory, believing that formalisation is akin to writing those horrible set encodings of everything. Which I would agree would be akin to writing assembly. But Lean, Rocq and Agda are all based in type theory. Which means it is more like the highest level programming language you can imagine! You have all the powers of abstraction, but you still have to convince the type checker – i.e. no “trust me, bro” casting, or even questionable while loops (“I promise this loop finishes at some point”). These abstractions along with meta programming techniques (“tactics”) means that you can write readable correct proofs, but it takes effort. Math is extremely deep, and getting formalised all the way to the research frontier in a given subfield is a serious undertaking. reply solomonb2 hours ago | root | parent | next[–] I think a lot of people have never actually tried using a proof checker and are forming hot takes based on their imagined assumptions about how they work. For anyone reading this, here is a very small example proof that + is associative over Nats in Agda (written using 1lab style equational reasoning syntax): +-associative : (x y z : Nat) → x + (y + z) ≡ (x + y) + z +-associative zero y z = refl +-associative (suc x) y z = suc x + (y + z) ≡⟨ ap suc (+-associative x y z) ⟩ suc (x + y + z) ≡⟨⟩ (suc x + y) + z ∎ We pattern match on the first nat to get zero and suc x. In the zero case we have 0 + (y + z) = (0 + y) + z. Both sides compute to y + z and thus the equation holds by reflexivity. In the suc x case we need to show that suc x + (y + z) ≡ (suc x + y) + z. suc x + (y + z) computes to suc (x + (y + z)) by the definition of +. By recursively calling +-associative x y z we get x + (y + z) ≡ (x + y) + z. Then we need to prove that by congruence this is true under suc. We get this by passing our proof (from the recursive call to +-associative) into ap suc. ap says that given a = b it is true that f a = f b. Finally, (suc x + y) + z computes to suc ((x + y) + z), so the last step holds by computation, which is why it’s just ≡⟨⟩. Proof checkers like Lean/Agda/Rocq are literally total functional programming languages with rich type systems. Everything above comes down to pattern matching and function application. The proof is just a function whose type is the statement we wanted to prove, and the type checker accepting it is what makes it a proof. This is the Curry-Howard Correspondence in a nutshell. Propositions are types and proofs are programs. reply black_knight1 hour ago | root | parent | next[–] And here is another short and simple example of some Agda code (Did you know you can open modules in a type signature‽): -- An element has at most one two-sided inverse. inverse-unique : ∀ (M : Monoid) (open Reasoning M) (x y z : type M) → y ⋆ x ＝ unit M → x ⋆ z ＝ unit M → y ＝ z inverse-unique M x y z leftInverse rightInverse = begin y ⟪ sym (unitᵣAt y) ⟫ y ⋆ unit M ⟪ mapᵣ (sym rightInverse) ⟫ y ⋆ (x ⋆ z) ⟪ sym (associativeAt y x z) ⟫ (y ⋆ x) ⋆ z ⟪ mapₗ leftInverse ⟫ unit M ⋆ z ⟪ unitₗAt z ⟫ z ∎ where open Reasoning M Not sure if all the unicode characters will render on HN, but the things left of the ⟪ ⟫-brackets is exactly what a text book in mathematics will have. While the things inside the brackets are just a functional-programming way of saying out the argument which would be left for the reader to make in their head for why each step holds. (If you know Agda, I dare you to look carefully at this example!) reply zelphirkalt4 hours ago | root | parent | prev | next[–] Assembly doesn't give you any safety or guardrails. It is basically the opposite. I think it would be a better comparison with something that is a very strictly typed and type checked language. reply pjmlp15 hours ago | root | parent | prev | next[–] Once upon a time this was all there was, so it naturally was proven to work as it was easier than dealing with boards full of dip switches that predated them. Naturally eventually we got macro Assemblers, followed by other attempts until FORTRAN came to be. reply nickysielicki18 hours ago | prev | next[–] Is that because you were starting from scratch and working alone, though? Imagine a hypothetical project at the scale of the Linux kernel, with thousands of mathematicians building up organized and well-commented code, standing on each others shoulders. reply ffaccount211 hours ago | parent | next[–] (not a mathematician, but I played with lean as a hobby). No, this already existed - lean standard library was basically this, with hundreds of mathematicians working together to formalize basics of currently known math. But this is just very slow for a human. I remember there being whole research groups trying to formalize a single (real world, as opposed to undergraduate) proof, and I remember reading that formalizing something like FLT is currently completely unfeasible. In short, no, lean was not a tool to discover new math. reply griffzhowl11 hours ago | root | parent | next[–] > formalizing something like FLT is currently completely unfeasible. No, Kevin Buzzard is leading a project to formalise FLT for a couple of years now. Anthropic scooped him last month, but his project involves more than just producing a formal proof: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h... reply olmo231 hour ago | root | parent | prev | next[–] Anthropic formalized FLT in 11 days: https://www.anthropic.com/research/formalizing-fermats-last-... reply anonymous90821318 hours ago | prev[–] Make a trivial adjustment to your final proposition and it would still hold, no? > Humans have quite a bit of creativity but make a lot of mistakes. The Lean typecheck never makes a mistake but has no creativity. Get them to work together in an iterative loop and you get what we have now. reply rcxdude9 hours ago | parent | next[–] It's less useful, because humans make fewer mistakes and take longer to turn their thoughts into Lean. I think most mathematicians have a higher success rate thinking about the problem informally, poking at it themselves, then formalizing it iteratively to make it more watertight as they gain confidence in the idea. reply dnautics4 hours ago | root | parent | next[–] > humans make fewer mistakes Is this empirically measurable? reply AxEy18 hours ago | parent | prev[–] The speed matters massively. Also it seems that LLMs are... getting to be quite creative. The point is that the there has to be an idea to try to check. Lean does not give you that. reply altmanaltman17 hours ago | root | parent[–] But a human being using LLMs will be much more creative than just LLMs alone right? Or does the human reduce the creativity in this system in your opinion? reply AxEy17 hours ago | root | parent | next[–] > But a human being using LLMs will be much more creative than just LLMs alone right? I believe so. But the question I was responding to was whether humans working with Lean would be have been more creative. reply eru14 hours ago | root | parent | prev[–] > Or does the human reduce the creativity in this system in your opinion? Yes. Humans are slow. reply
Consider applying for YC's Winter 2027 batch! Applications are open till November 2. Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact Search: