infruset

> "Georges Gonthier, a computer scientist at Inria in Paris"

somehow the article forgets to mention he was the guy who came up with the first Coq (now Rocq) formal proof of the Four Color Theorem..

"Two early 20th century authors are talking while walking downtown Paris, occasionally noticing landmarks, while we hear horse hooves as well as a few cars"

https://stableaudio.com/1/share/b4eeaa11-cf29-4e09-88cd-a058...

Note there is a fork oh-my-pi: https://github.com/can1357/oh-my-pi of https://blog.can.ac/2026/02/12/the-harness-problem/ fame. I use it as a daily driver but I also love pi.

So as for math of that level, (the best) humans are still kings by far. But things are moving quickly and there is very exciting human-machine collaboration, one need only look at recent interviews of Terence Tao!

I can't disclose that, but what I can say is no one at my company writes Lean yet. I'm basically experimenting with formalizing in Lean stuff I normally do in other languages, and getting results exciting enough I hope to trigger adoption internally. But this is bigger than any single company!

I was waiting for a post like this to hit the front page of Hacker News any day. Ever since Opus 4.5 and GPT 5.2 came out (mere weeks ago), I've been writing tens of thousands of lines of Lean 4 in a software engineering job and I feel like we are on the eve of a revolution. What used to take me 6 months of work when I was doing my PhD in Coq (now Rocq), now takes from a few hours to a few days. Whole programming languages can get formalized executable semantics in little time. Lean 4 already has a gigantic amount of libraries for math but also for computer science; I expect open source projects to sprout with formalizations of every language, protocol, standard, algorithm you can think of.

Even if you have never written formal proofs but are intrigued by them, try asking a coding agent to do some basic verification. You will not regret it.

Formal proof is not just about proving stuff, it's also about disproving stuff, by finding counterexamples. Once you have stated your property, you can let quickcheck/plausible attack it, possibly helped by a suitable generator which does not have to be random: it can be steered by an LLM as well.

Even further, I'm toying with the idea of including LLMs inside the formalization itself. There is an old and rich idea in the domain of formal proof, that of certificates: rather than proving that the algorithm that produces a result is correct, just compute a checkable certificate with untrusted code and verify it is correct. Checkable certificates can be produced by unverified programs, humans, and now LLMs. Properties, invariants, can all be "guessed" without harm by an LLM and would still have to pass a checker. We have truly entered an age of oracles. It's not halting-problem-oracle territory of course, but it sometimes feels pretty close for practical purposes. LLMs are already better at math than most of us and certainly than me, and so any problem I could plausibly solve on my own, they will do faster without my having to wonder if there is a subtle bug in the proof. I still need to look at the definitions and statements, of course, but my role has changed from finding to checking. Exploring the space of possible solutions is now mostly done better and faster by LLMs. And you can run as many in parallel as you can keep up with, in attention and in time (and money).

If anyone else is as excited about all this as I am, feel free to reach out in comments, I'd love to hear about people's projects !

Does anyone have a clue how far we are from having "LLMs for animals"? Even if we don't understand what the LLM is saying to a dolphin or a monkey, does it change much from feeding millions of texts to a model without ever explaining language to it as a prerequisite?

Very nice ! How might one go about adapting this to other languages ? Does a version of the model downloaded exist somewhere ?

I think they are the conference and journal versions of the same paper. Hadn't seen it was mentioned in the article, I should have read it more thoroughly!

If on top of rigorous, you want them to be formally verified in Coq at the same time as they are computed: https://www.lri.fr/~melquion/doc/18-jar.pdf

Can it be pointed to a remote ollama server ?

It's interesting that historically, in France, the more prestigious a publisher is, the more bland the cover. Book covers with colors all over the place feel cheap over here.

I've read it, and I warmly recommend it! And it is true and ironic that the only language I could read it in was.. English

Random people from all these countries can name of the top of their head a bunch of any of the following:

- US presidents

- US pop artists

- US filmmakers

- US cities

- US CEOs

- US companies

- US TV shows

I stopped there but I could go on for long. Now, take any country X other than the US and ask a random resident of any of the other countries to name just one of each category: a president of X, a CEO, a film, etc... If you think the answer has any chance to compete with the equivalent question asked of the US, well, I think you don't realize how big the cultural influence of the US is. What is domestic news in the US is still news in the rest of the world, but the reverse is simply not true.

Thanks for the link! And I really appreciate any work about books, really, and yours is of great magnitude, thanks for sharing your project. If you ever look to expand it to French, I could be interested in helping.

Well, I don't think anyone in particular is to blame; I'm guessing Danish publishers and booksellers cater to their public and have little economic leeway to risk translating risky books for a small linguistic group. That's the problem, it's the effect of the forces at play in a global free market economy dominated by the English language: we all have to roll over and make way for what sells, regardless of the respect literatures and languages otherwise deserve.

> You are fully welcome to go and look at these places as well; they are also global in the same sense that y combinator is.

Allow me to respectfully disagree: they are not. The dominance of US culture around the world, for the best and for the worst, is a fact of life for all of us who live outside it. If you look at the rates of translation of books from and to English, you will immediately see where the center and the periphery lie.

Thanks for your answer. I will try to clarify a bit.

Of course we all know the books are going to be written in English. I am not trying to ask for an idiot-proof label stating the obvious lest a reader might waste a click expecting German-language books.

The point I am trying to make is that the word "book" in the dominant anglosphere has come to mean almost exclusively books coming from an English-speaking country (and even among those I'm sure the proportions are skewed towards the US/UK, although I would be happy to be disproved). So if I discuss "books" in an English conversation (English being the language we are all forced to speak globally now) it is often implicitly expected that we are discussing those books, the books of the anglosphere. Some food for thought, less than 1% of books read in the US are translations[0], which is not the case in other countries (if only because a lot of countries read a lot of translated books from.. English).

> If I was visiting a site written entirely in French I would have zero expectation that any book list would clarify that the books are French language

This comment seems to assume that all languages are equal and interchangeable; they are not. This is maybe hard to realize from within the English-speaking global culture, but other languages are now vassals of English. What I'm saying is that it would be a small act of acknowledgement of this hegemony to remember what is being left out of the conversation.

[0] https://lithub.com/why-do-americans-read-so-few-books-in-tra...

There would never be a site/post "les cent meilleurs livres de 2023" on a global discussion board such as this because by definition it would not be in English. There might be a "the best french books of 2023" post, although there wouldn't be, because French books simply don't exist in the anglosphere, but my point is precisely that the global conversation happens in English, the only word that ever reaches it is "book", and it's never about anything else than English books.

I get that HN is an english-language website from the US, and that I'm not entitled for this website to include me. Don't take this as personal criticism -- if anything I like your project --, I'm hating the game and not the player. But the english language and US/UK culture are hegemonic today, which means people from all around the world read and write the words "book" and "author" on HN without realizing, or realizing too well, depending on who they are, that what is actually meant is "english-language books" (including a moderate amount of translations, thank goodness) and "english-speaking authors" (a majority of whom are American or British, even when they are immigrants). I'm not sure this comment will do anything, but someone had to say it, maybe just to maintain a modicum of awareness that millions of books are written in other languages and never make it to the english-speaking eye, and are thus buried alive as not-really-books and their writers not-really-authors in the global conversation. Maybe the relevant adjectives ("english-language", "American", "British") might be used more to remind readers that by "books" we do not mean "all books", but "books accessible in the US"?

I've seen the same reaction from people learning to program. Why are there thousands of programming languages? Why not put everything under one standard?

The main answer, as for many variations of this question (languages, laws, units of measure, programming languages), is history. Efforts to formalize mathematics have spawned in different universities, at different times, in different teams with different cultures and approaches. The mathematical theories underlying the software also vary greatly. There isn't one agreed upon formalization of mathematics. There's classical logic and there's intuitionistic logic, which wants to see every existence theorem backed by an actual witness and does not agree that `not (not A) = A`. (Speaking of which, different systems have (very) different notions of equality! In case you thought this one would at least be simple). Sometimes two pieces of software have nearly identical foundations, such as Lean and Coq to some extent; but one is decades old, and the other is a rewrite from scratch using other unification algorithms and a different programming language. Sometimes people just don't get along and start competing projects.

Note that some people have intended to unify various proof systems, which reminds me of the classical https://xkcd.com/927/

Do any commercial domestic solutions exist?

I have the same question, and more generally: Any generic way of doing this for any of the open source or semi open source models, especially Mistral[0]?

[0] https://news.ycombinator.com/item?id=37675496

> Encompasses Replit's top 30 programming languages with a custom trained 32K vocabulary for high performance and coverage

Any idea where the list can be found?