Email Gateway (Aug 22 2022 at 18:05): Email Gateway (Aug 22 2022 at 18:05):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
A beautiful number-theoretic application of the undecidability results of
Minsky Machines is J. Conway's proof of the undecidability of the
generalized 3x+1 problem. Paul Erdos commented, concerning the
intractability of the original 3x+1 problem: Mathematics is not yet ready
for such problems.
http://mathworld.wolfram.com/CollatzProblem.html
So, a formal verification in Isabelle/HOL of Conway's proof could be a nice
way to apply the Minsky Machines library to a mathematical result which is
important in contemporary number theory.
https://www.isa-afp.org/entries/Minsky_Machines.html
If someone is interested at looking at Conway's proof, which is extremely
simple and elegant, the name of the paper is
Conway, J. (1972). Unpredictable iterations,
which can be found in the following book (page 219):
Jeffrey C. Lagarias, The Ultimate Challenge: The 3x+1 Problem
https://www.amazon.com/Ultimate-Challenge-3x-Problem/dp/0821849409
Kind Regards,
Jose M.
Date: Tue, 14 Aug 2018 11:36:18 +0200
Last updated: Nov 21 2024 at 12:39 UTC