Post #2636081

2026-05-05 15:02 UTC

@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?

Replies (2)

@JacquesC2@types.pl 2026-05-05 18:36

@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.

Open ##2636082
@iblech@mathstodon.xyz 2026-05-05 22:46

@andrejbauer@mathstodon.xyz @JacquesC2@types.pl (off topic and inconsequential) Well, as you know, there is the *universal algorithm*. This algorithm has the property that, for every function f : ℕ → ℕ, there is a universe such that, when run there, it computes exactly f [on all standard inputs]. But this universe does not contain a proof of this fact. Indeed, it contains a disproof. :-) Newcomers to the universal algorithm might enjoy this introduction: https://juliakw.net/research/talks/2020-oct-universal-algorithm/univ-alg.pdf (slides by Kameryn Williams)

Open ##2636083