I find it really strange that people who don't use lean don't just get on and use the alternatives rather that trying to get everyone who is using lean to use something else. It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs.

It's important to meet reality head on: Every mathematician is not going to collaborate on the same tooling (as wonderful as that might seem on the surface to be as an outcome) human beings are different and want different things, and people are productive in different environments. In particular, people who want to formalize results within the standard framework (including zfc) are never really as a group going to care that much that lean4 doesn't let them formalize results outside of zfc.

▲

Balooga a few seconds ago | parent | next [-]

> It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs.

That's why emacs has a vim mode[1].

[1] - https://github.com/emacs-evil/evil

▲

wk_end an hour ago | parent | prev | next [-]

> It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs.

I don't know about forcing, but there's certainly a long history of emacs users trying to convince vim users that they're wrong. Without loss of generality - the same is true in the other direction of course.

Software devs are more than used to having a multitude of tools at our disposal (text editors, programming languages, Linux distros...), having strong preferences, and engaging in the delicate balancing act of advocating for our favourites while living-and-letting-live as the cosmic ballet goes on. It's part of our culture; I don't think that culture necessarily exists outside. For instance, a common layman question to ask is, "Why are there so many programming languages? Why doesn't everyone just use the same one?" And I don't think mathematicians are immune to this blind spot.

The nearest equivalent to "tooling" in math, traditionally, would be notation I suppose, and mathematicians are accustomed to eventually coalescing around a single standard notation.

▲

quasisphere 2 hours ago | parent | prev | next [-]

Agreed. In addition I think a big reason why we are discussing formalization so much at the moment is that it has only recently become viable to do large scale formalization of mainstream mathematics, using LLMs. These same LLMs will make it much easier to translate from one language to another and port even larger codebases over.

My prediction would therefore be that the LLMs will let us work more-or-less using standard mathematical prose that then gets to codified to some machine-readable and checkable language, but what the language used by the proof checker actually is will be more of a technical detail. In particular, I suspect people will not care too much about the language used for proofs themselves, which means that we might allow for more boilerplate if it is faster to elaborate/compile, unlike current interactive theorem provers which are meant to ease the work of humans. How the language looks like for the statements of the theorems and definitions is probably more important however, since humans will want still to be able to check that what is being formalized corresponds to what they had in mind.

▲

voxl 2 hours ago | parent [-]

This is horseshit. Mathlib3 and mathlib4 all existed prior to LLMs. Unimath of Agda, mathematical components of Rocq, the list goes on.

LLMs have done nothing for "making large scale mechanization viable." They have been viable. The only thing has changed is the perception of the random developer who never wanted to put the effort into learning what actually needed to be learned and are instead happy to spit our complete garbage, spec and all, and say it's a proof of something.

It's not shocking at all that the people who seem to get any benefit out of LLMs in the proof assistant space are the ones who could have just don't it themselves anyway.

▲

quasisphere an hour ago | parent [-]

I actually noticed after I posted that I should have said 'by individuals at pace not too different from writing down a standard prose proof' or something similar to address this point. Mathlib for instance is of course a phenomenal project, but it was written by a large amount of people over many years. Granted their goal was not so much speed as it was elegance, but by 'viable' I had in mind something that a research mathematician could actually use in real time along actual math research. The content in Mathlib still falls very much short of being enough for formalizing much of the actual research being done in mathematics, but people are now autoformalizing non-trivial extensions on top of that, both individually and collaboratively (such as the recent Tau Ceti project).

Anyway, what do you mean by 'say it's a proof of something'? If you mean this in technical sense, there are plenty of examples around where single individuals or small teams have autoformalized theorems with tens or hundreds of thousands of lines Lean code that pass a comparator challenge (so the theorem is correct). If you mean this in the sense that the proof is also a proof in the eyes of humans, so that someone has actually read or understood the proof, I'm willing to acknowledge that in this area there is much work still to do. In my own experience the current LLMs are already very strong at formally proving theorems (with correct semantics), but they are still lacking in writing human-readable math prose based on these formalizations, for instance.

	▲	wizzwizz4 22 minutes ago \| parent [-]
		> The content in Mathlib still falls very much short of being enough for formalizing much of the actual research being done in mathematics, but people are now autoformalizing non-trivial extensions on top of that, Formalising non-trivial extensions on top of the standard library is not hard. I could bash out an average textbook formalisation at about half reading speed. The hard part is making something elegant and general, which: and that's something that LLMs don't seem able to do.¹ (If you're lucky, the textbook you're working from has already distilled the best abstractions, and there's very little work left to do to make it good enough for a library: but such textbooks do not exist in research mathematics.) > Granted their goal was not so much speed as it was elegance, Do not underestimate the necessity of mathematical elegance. Mathematical notation is a tool powerful enough to teach machines to think: it is essential to make these tools elegant, or you will not be able to communicate your insight to your colleagues, and certainly not the next generation. Treating the goal of mathematics as "prove the most theorems as fast as possible" is hacking off the lower branches we should be using to climb trees, simply to harvest their fruit. ¹: Anyone familiar with my HN comment history will know that I keep banging on about "cannot in principle" and "there are deep theoretical reasons that an LLM can never". I'm not doing that here: I don't know a reason that LLMs can't produce elegant mathematical abstractions – probably because I don't understand mathematics deeply enough: "LLMs can't do this" is purely an empirical observation. (Believe me, I've read a lot of LLM-generated formal mathematics: it is invariably garbage. I just don't know why.)

▲

data-ottawa 2 hours ago | parent | prev | next [-]

I think it’s a lot like R vs SAS or Python and not any departure from the norm.

Mathematicians are not highly technical users that generally like programming. If you give them a path of importing someone else’s work they’ll do that instead of redoing it in their theorem prover of choice.

See the old mathematician joke:

A mathematician is asked to make tea. They take the kettle from the shelf, fill it with water, put it on the stove, turn on the heat and boil the water, then pour it into a cup.

The next day someone asks the mathematician to make tea again. The kettle is still on the stove from yesterday and there’s some leftover water in it, enough for tea.

The mathematician dumps the kettle out and puts the it away on the shelf. The mathematician says the system is in a known previously solved state and therefore trivially solved.

Now substitute 1500 lines of coq or lean for the kettle. As far as I know the outputs aren’t interchangeable like a vim or eMacs text file.

▲

pverheggen an hour ago | parent | prev | next [-]

I have zero experience with formal verification, just speculating here - but could it be because of the network effects?

More users on your preferred tool means a more comprehensive database of existing proofs, and that makes writing new proofs easier, right?

	▲	seanhunter 29 minutes ago \| parent \| next [-]
		Absolutely that's the reason. But the point is the big communities (I'm thinking https://leanprover-community.github.io/ , Kevin Buzzard and all the stuff he's got going at imperial college in the uk etc, the analogous efforts around roq, agda etc which I'm not as familiar with) have made their respective choices and are just getting on with formalising maths. Then there is a vocal minority who want to sit on the sidelines and say they want all these people to use something different from what they have already decided to use. Seems weird.[1] But yeah it is definitely easier if you just need to formalise the piece you are working on and not invent the whole universe just to bake an apple pie. [1] And I know it's exactly the same as the people on here and other forums who say other people should down tools on project X and rewrite it in go/rust/zig/whatever. I find that weird also. Like if you want to rewrite a thing in a different language go do that by all means. But saying someone else who develops something in their own time should instead develop a different thing or use a different language is just weird.
	▲	joe_the_user an hour ago \| parent \| prev [-]
		I too know nothing about formal verification but I know that mathematical proof is different individual tooling. Informal statements, Lean and whatever other formal provers are all language and languages are social so what someone uses will impact you and so it's legitimate to have an opinion.

▲

andrewflnr an hour ago | parent | prev | next [-]

Presumably because of potential network effects that would result from everyone being able to work in a single system. I don't think it's strange or implausible for people to want that.

▲

ux266478 3 hours ago | parent | prev [-]

> lean4 doesn't let them formalize results outside of zfc.

A small correction: Lean 4's native semantics are DTT, not ZFC. Formalizing results for TT is arguably easier, it's the default. But you can use it for any foundation, so long as you have an implementation.