@JacquesC2 @andrejbauer @soaproot @dimpase
I'm a bit confused. When the CAS pseudo-algorithms do work, there is some informal reasoning that the output is correct that in principle could be formalized in the next 100 years. Some of what they do is equational search / term rewriting for which reasonable certificates would be the chain of steps. I don't see how being in NP or worse impacts the feasibility of producing certificates for particular solutions. SAT solvers certainly can produce certificates when they succeed.
=> More informations about this toot | View the thread | More toots from sandmouth@types.pl
=> View JacquesC2@types.pl profile | View andrejbauer@mathstodon.xyz profile | View soaproot@sfba.social profile | View dimpase@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).