Hofstadter's problem for curious readers
Pierre Letouzey
TL;DR
This paper summarizes Coq-based proofs related to Hofstadter's G function and its flipped variant, exploring their properties and connections to infinite trees, as inspired by Hofstadter's problem for curious readers.
Contribution
It provides formal proofs and analysis of Hofstadter's G function and its flipped variant using Coq, contributing to the understanding of these recursive structures.
Findings
Formal verification of Hofstadter's G function properties
Analysis of the flipped G tree variant
Connections to OEIS sequences A005206 and A123070
Abstract
This document summarizes the proofs made during a Coq development inSummer 2015. This development investigates the function G introducedby Hofstadter in his famous "G{\"o}del, Escher, Bach" bookas well as a related infinite tree. The left/right flipped variantof this G tree has also been studied here, followingHofstadter's "problem for the curious reader".The initial G function is refered as sequence A005206 inOEIS, while the flipped version is the sequence A123070.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputability, Logic, AI Algorithms · Advanced Mathematical Theories and Applications