Andrej Bauer

@johncarlosbaez@mathstodon.xyz @dougmerritt@mathstodon.xyz @MartinEscardo@mathstodon.xyz @JacquesC2@types.pl @pigworker@types.pl Somewhat unexpectedly, I find myself on the same side as @xenaproject@mathstodon.xyz on this one, I suppose because I read "the right way" differently from @johncarlosbaez@mathstodon.xyz Formalized mathematics makes us think "the right way" in the sense that it requires mental hygiene, it encourages better organization, it invites abstraction, and it demands honesty. Formalized mathematics does not at all impose "One and Only Truth", nor does it "nail things down with rigidity" or "impose concensus". Those are impressions that an outsider might get by observing how, for the first time, some mathematicians have banded together to produce the largest library of formalized mathematics in history. But let's be honest, it's miniscule. Even within a single proof assistant, there is a great deal of freedom of exploration of foundations, and there are many different ways to formalize any given topic. Not to mention that having several proof assistants, each peddling its own foundation, has only contributed to plurality of mathematical thought. Current tools are relatively immature and do indeed steal time from creative thought to some degree, although people who are proficient in their use regularly explore mathematics with proof assistants (for example @MartinEscardo@mathstodon.xyz and myself), testifying to their creative potential. Finally, any fear that Mathlib and Lean will dominate mathematical thought, or even just formalized mathematics, is a hollow one. Mathlib will soon be left in the dust of history, but it will always be remembered as the project that brought formalized mathematics from the fringes of computer science to the mainstream of mathematics.

@tao The research group around Sylvie Boldo has done a great deal of work on verified computer arithmetic in Rocq, in case you ever have to go beyond 17th century methods. For example, they formalized numerical methods for Lebesgue intergration. Here are some relevant links for reference: https://pages.saclay.inria.fr/sylvie.boldo/research.html https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis P.S. I should also mention Assia Mahboubi and https://fresco.gitlabpages.inria.fr – their work is quite relevant here as well.

@JacquesC2@types.pl That's how I feel about Theory A papers titled "A provably correct algorithm for ..." Do they also publish incorrect algorithms? Or ones that are correct but somehow it's not provable that they're correct?

@boarders Please send me your home address. I have prepackaged several bags of dried peas, with instructions on how to execute penance.

@danielgratzer Just make sure to use an unreliable calendar that can plausibly drop events for no good reason. (If you wear glasses, make sure to check the calendar without glasses when you plan events.)

@dginev@mathstodon.xyz Right, so really I should buy my AI a desktop. Interesting development.

@jonmsterling This is how Facebook started.

So after some suffering it turns out that the main culprit is jupter-book version 2, which has nothing to do with version 1. Someone has a sick sense of humor when it comes to naming software. Reverting back to version 1 made life much easier (and also non-dependent on typst).

@jonmsterling But what's the solution?

@iblech@mathstodon.xyz @JacquesC2@types.pl Somehow I suspect Theory A people don't have that sort of thing in mind, but one should certainly attempt to publish an algorithms paper along these lines, maybe on April 1.

@xameer@mathstodon.xyz We'll cross that bridge when we come to it. I am not into theoretical real life situations.

@xameer@mathstodon.xyz Dual, as in those cases one convinces the customer that the product is not human.

@wtgowers Close, close, but not quite there.

@fl Claude converted my 20+ year old Perl script which generated the web pages to a Python script, converted the Perl lists describing the data to JSON, improved CSS, etc.