I'd love it if there was a tradition of putting in an "author's version" of a paper onto the arxiv. No, I don't mean the extended version, I mean the version with all the puns, side stories, footnotes and the like kept in. And sure, the proofs too.
Remote
Jacques Carette
@JacquesC2@types.pl
mastodon 4.8.0-alpha.2+glitchComputing Scientist, ex-mathematician. Currently in academia, spent considerable time in industry as well. Into weird programming languages and the outer parts of programming and software engineering. Currently exploring metaprogramming, quantum programming, DSLs and "generate everything".
857 Followers
367 Following
46 Posts
Joined May 03, 2022
When even the abstract is complete nonsense. Sigh.
I think I like doing work with a proof assistant for exactly the reason that drove others nuts: there is nowhere for tacit knowledge to hide.
I was reminded of this while trying to read some "paper math" on type theoretical forcing. I can't just click on some bits to ask "what exactly do you mean by this part here". [The thing I wanted to know was indeed never defined, just assumed to be known.]
This is the point of formalization:
In several places, the process of formalization sharpened our understanding
of the informal presentation.
p. 4 of a just-landed formalization of the reals in cubical agda. https://users.cs.utah.edu/~blg/resources/pdf/jackson-brough-cubicalreals-2026.pdf
No one who has done enough proving should ever say that a "program has been proven correct."
Does it satisfy the theorems you've proven? Sure. Are they all the theorems needed to say 'correct'? Extremely unlikely!
"We present a sorry-free formalization" -- as if a document with 'sorry's in them could be called a formalization?
@egbertrijke@mathstodon.xyz
I quite like formalizations that are made to look like encyclopedia pages.
I just dislike when they are made to serve double-duty, i.e. serve a narrative purpose as well as a "source code for a library" purpose at the same time. Then you're forced into all sorts of compromises.
Libraries need vastly different organization than good narrative does.
I don't actually care which one ends up being the primary artifact. [But my current best guess is that it's easier to put a narrative atop a well-organized library than the other way around. I'd be happy to be shown otherwise.]
Replying to
@johncarlosbaez@mathstodon.xyz @dougmerritt@mathstodon.xyz @MartinEscardo@mathstodon.xyz @andrejbauer@mathstodon.xyz @pigworker@types.pl I would compare Lean+Mathlib to Java rather than FORTRAN and Pascal: Java is just as boring a PL as others, but it is a much stronger ecosystem (IDEs, libraries, tutorials, etc). Thus developers have a much better experience using Lean+Mathlib and the surrounding ecosystem (blueprints are super cool, as just one example).
In my mind, it is purely 'social forces' that has made and is making Lean+Mathlib the apparent winner. And that has snowballed - almost to the point of smothering everything else, which is extremely dangerous for innovation.
When I agreed to be on the PC for conference X, I did not think I had agreed to review alchemy papers. And yet, here we are.
Yes, this is about "modern AI".
Replying to
@simon@fedi.simonwillison.net I guess this is what happens when you have Kabayashi Maru in your training set?
Replying to
Replying to
@johncarlosbaez@mathstodon.xyz @dougmerritt@mathstodon.xyz @MartinEscardo@mathstodon.xyz @andrejbauer@mathstodon.xyz @pigworker@types.pl On a more personal note, I'm strongly enjoying that all this work on proof assistants is forcing many many more people to think about meta-mathematics (and I don't mean just logic here, but all aspects of 'mathematics' as a subject of study.) /end
Replying to
@maxsnew@types.pl @mc@mathstodon.xyz It's so freaking weird being the 'old' one around witnessing the young people making the next generation of good stuff.
But I console myself by thinking that I'm excited by it all rather being grumpy about it.
Now this is the kind of software engineering research that I'd like to see more of! https://arxiv.org/abs/2602.10540
It would be hilarious if what un-scaled university classes (i.e. pushed them to be smaller) was LLMs.
If a class is supposed to be teaching students some skills, then we can no longer check if that has been successful "remotely" (i.e. via written assignments). So we have to check them in-person. Which takes a lot more time.
Listening to a bunch of Bee Gee's stuff right now. My, they were so good!
Yes, I like them. And Lorna Shore and Rammstein and Rush and Metric and Abba and Avril Lavigne and The Hu and Nusrat Fateh Ali Khan. And so many more.
Replying to
@MartinEscardo@mathstodon.xyz
Your main point remains: doing new mathematics with a theorem prover as blackboard is different. I've done that too, I love it, and fully agree that it is both pleasurable and very different than writing either a library or an encyclopedic reconstruction.
However, allow me to be pedantic for a moment: pretty much everyone who has formalized category theory, in particular, comes to hate how it is organized in textbooks. I know agda-categories is seriously sub-optimal because it follows the classical organization way too much. Other formalizations are better for having thrown off those shackles!
There are similarly lots of papers, indeed from the mathlib people, who report the same: the classical textbooks were not the best source. And, of course, same is true for MathComp in Rocq.
@egbertrijke@mathstodon.xyz @gallais@mamot.fr
Replying to
@MartinEscardo@mathstodon.xyz Welcome to the joys of a particular flavour of meta-mathematics.
From every system (Mizar, Rocq, mathlib, Agda, Isabelle/HOL for sure), I've heard people who have dug into the de facto dependency graph marvel at how unexpected it is.
These modern tools ought to be used to teach us how mathematics is actually organized.
Replying to
@MartinEscardo@mathstodon.xyz
Note that I also like story-like narrative.
My main points remain:
the needs of libraries and narrative are very different (and thus need different solutions)being bound to 'files' as a unit of source is a bad idea
When you read a paper, you read the PDF, not the LaTeX source, right? Why should Agda be any different?
@egbertrijke@mathstodon.xyz @gallais@mamot.fr
Replying to
@johncarlosbaez@mathstodon.xyz @dougmerritt@mathstodon.xyz @MartinEscardo@mathstodon.xyz @andrejbauer@mathstodon.xyz @pigworker@types.pl On the more optimistic side:
there is a lot of structure to mathematics, which is currently not very well leveraged, i.e. Universal Algebra and its many generalizations. But people are working on that (myself included).regardless of what some say, there is a lot of 'computational mathematics', which is currently not well supported by any system, and essentially eschewed by Lean+Mathlib. That requires thinking differently. Again, people are working on that.in fact, there is quite a bit more to math in general -- see the Tetrapod approach for one.
To me, what's really missing are experts in designing UX having a solid look at mechanized mathematics tools. For that to bear fruit, experts in requirements analysis need to better understand the full "mathematics workflow" -- where proof is just one small aspect. It might indeed be the most time-consuming part, but it is not necessarily where the most value lies. [See LaTeX as an example of a strong value proposition that has completely changed the practice of mathematics, but in a surreptitious way, as it is essentially invisible wrt "mathematical thought". Its effect is no less important.]
Replying to
@maxsnew Not sure how to vote. You should absolutely re-learn abstract algebra. Should you learn algebraic geometry? Less sure.
Damn. I jotted down a quick idea in my research notes file (in markdown, in github, using the web edit function). Copilot auto-filled a commit message as a starting point. It was good. That is super annoying.
github crumbling because of AI is both sad and funny.
And annoying: can't do my code reviews right now.
Replying to
@johncarlosbaez@mathstodon.xyz @dougmerritt@mathstodon.xyz @MartinEscardo@mathstodon.xyz @andrejbauer@mathstodon.xyz @pigworker@types.pl I can give it a try.
First: Lean and Mathlib embody a very particular philosophy. Lean 4 aims to be "practical", which is mainly code for 'allowing lots of automation'. It cuts some serious corners to achieve that (others have written about that at length). Mathlib chooses to be a 'monorepo' (which is laudable indeed IMHO). The combination of Lean's technology choices and the monorepo decision is what forces 'consensus'.
Replying to
@johncarlosbaez@mathstodon.xyz @dougmerritt@mathstodon.xyz @MartinEscardo@mathstodon.xyz @andrejbauer@mathstodon.xyz @pigworker@types.pl Are there specific ideas around to make things better? Absolutely! Heck, there are old ideas (Epigram comes to mind, but even Automath has not been fully mined yet) that are still not implemented.
I will continue later - need to attend to other things right now.
Hard puzzle: what do Perth, Scotland and Erfoud, Morocco have in common?
[Answer might be delayed, wifi connection where I am is not necessarily good.]
Replying to
@pigworker@types.pl Hoo, I needed a better name than "proto data", "predata", "data chunk" -- now I've found it.
Replying to
@mc@mathstodon.xyz If the contribution is the formalization, there are journals for that. In other publication venues, the main contribution should be something else, supported by the increased certainty of formalization.
Unless the formalization teaches us something new, and that's the main point. But that's getting considerably harder to achieve.
In general I see the point of publishing as teaching the readers something new, of interest.
Replying to
@maxsnew@types.pl @mc@mathstodon.xyz This! So much this!
Max (and his group) is exploring around, thoroughly exploring non-orthodox definitions while being guided by definitely categorical thinking. [Ponder that paradox for a second.]
I have no idea which of these will come out to be better than what's been done before -- but I'm super excited by being able to witness all this exploration.
Replying to
@mc@mathstodon.xyz
By 'it', I assume you mean category theory?
There is no write-up that I know of. But if you read the 1lab and @maxsnew@types.pl 's cubical-categorical-logic, you'll get a good idea of where people are going.
Replying to
@de_Jong_Tom@mathstodon.xyz @gadmm@mathstodon.xyz My understanding is that some of the core Agda devs who do extremely valuable but super tedious development want to be able to use AI to ease that burden. Which doesn't sound so bad, until you dig deeper into what "using AI" entails.
Replying to
@Taneb@hacksrus.xyz Whatever you find, I'm interested too!
Beyond Parnas' principle of information hiding (i.e. each module keeps a set of secrets that no other module can have), I don't know of anything useful. The OO crowd has written all sorts of stuff, but it all seems either 'meh' or a corollary of Information Hiding.
Replying to
@johncarlosbaez@mathstodon.xyz @dougmerritt@mathstodon.xyz @MartinEscardo@mathstodon.xyz @andrejbauer@mathstodon.xyz @pigworker@types.pl I agree with @andrejbauer@mathstodon.xyz 's take, including his skepticism of my comments on Lean choking things off: we're talking (implicitly) about different time scales. I'm witnessing a current funnelling of resources, which will cause short-term pain. Indeed this is unlikely to remain 'forever'.
Replying to
@maxsnew@types.pl @mc@mathstodon.xyz Yeah, I should have warned Matteo that your library requires serious archeological skills to peruse on one's own!
Having said that, Matteo definitely has the categorical chops to "get" what you're doing -- more so than me, frankly.
"Never hallucinate or make anything up." Sounds like instructions for the orange one at trial. Or instructions a reporter might wish to give before an interview.
Replying to
@MartinEscardo@mathstodon.xyz
Hopefully we'll have occasion to meet in person in a setting where we can discuss all of this at leisure.
I think the outcome of such a discussion is likely to be:
1) an "oh, I see" from you,
2) a continued "happy to disagree"!
I liken it to (say) the main ocaml and haskell developers meeting to compare notes. They learn a lot from each other but still leave with some core opinions unchanged. [I have personally witnessed this.] And yet each side has truly learned something.
@egbertrijke@mathstodon.xyz @gallais@mamot.fr
Replying to
@andrejbauer@mathstodon.xyz "We think it's correct but can't be bothered to check" ?
Or maybe it's like the Risch Algorithm: it is a correct algorithm for the problem in differential algebra that it solves, but it is an incorrect algorithm for computing closed-form integrals in analysis.
Replying to
@jpoiret Much of my recent work (especially lots of the as yet unsubmitted work) is proofs-first. Because the ideas are just strange enough that even I don't quite believe them until I have proofs of everything!
Replying to
@MartinEscardo@mathstodon.xyz @ltchen@mathstodon.xyz So completely on-brand for Larry then?
Replying to
@mc@mathstodon.xyz But of course, in some disciplines, doing an experiment that has never been done, collecting and analyzing the data, and publishing that, is regarded as valuable and new.
Replying to
@mc@mathstodon.xyz Amusingly, also re-inventing what IMPS, the theorem prover that few have even heard of, did 30 years ago.
Replying to
@mc@mathstodon.xyz I personally go bottom-up. So start at any file, and follow the dependencies until you find the files that have none, and read things on your way back up.
@maxsnew@types.pl
Replying to
@gadmm@mathstodon.xyz @de_Jong_Tom@mathstodon.xyz My best understanding is that the answer to 1. is "it depends" (!!!) and 2. is "probably".
However some of the very anti-LLM people have left [very sad, given the community is quite small], so I'm not sure exactly how that changes things.
Before the "it can be allowed" decision, some LLM code (by old timers) was allowed, and some LLM code (huge, by new people) was rejected.
The situation is extremely muddy.