Chaos and the Julia set of the complex exponential

Source: arxiv:1408.1129, doi:10.4169/amer.math.monthly.122.10.919, url:https://github.com/LR-UK/exp-chaotic Authors: Lasse Rempe Status: verified Main declarations: ExpChaotic.devaney_chaotic, ExpChaotic.juliaSet_exp Tags: complex-dynamics, exponential-map, julia-sets, chaos, holomorphic-functions MSC: 37F10, 30D05

Attribution and upstream scope

The proof development is from Lasse Rempe's LR-UK/exp-chaotic, commit 303b2d3d1121ebc3a86399de8f1e71c17a8b6dd8, first publicly released on 15 September 2026. The initial complete source commit is ec117ebcad069b7fe54acffdef2e3c4dab6bd982. The Lean proofs were primarily generated by AI under Rempe's direction, using Microsoft 365 Copilot, Claude, and ChatGPT. The twelve modules, including the public interface, are retained; upstream challenge placeholders, duplicate solution bridges, and audit scripts are outside this import.

The initial six-lemma proof architecture and related mathematical interface were adapted from John Harrison's Examples/misiurewicz.ml in HOL Light, introduced by commit 5b7d9abdbee087c67c958d1d2b9fe7ba9ffbe004 on 10 November 2014: https://github.com/jrh13/hol-light/blob/5b7d9abdbee087c67c958d1d2b9fe7ba9ffbe004/Examples/misiurewicz.ml

Harrison's formalization followed a challenge posed by Lasse Rempe-Gillen on the Foundations of Mathematics mailing list and communicated to Harrison by Freek Wiedijk. The Lean contributions are Apache-2.0. The following retained HOL Light notice applies to the adapted material; the Apache license does not remove or restrict it.