<figure><img src="image_1.png" /></figure>

HAL
open science

# A Formalisation of factorions in Rocq

Laurent Théry

► To cite this version:

Laurent Théry. A Formalisation of factorions in Rocq. Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France. 2025. hal-05265618

HAL Id: hal-05265618

https://inria.hal.science/hal-05265618v1

Submitted on 18 Sep 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A Formalisation of factorions in RocQ

Laurent Théry

STAMP project – Inria Center at Université Côte d'Azur

Laurent.Thery@inria.fr

## Abstract

This note explains how some basic properties of factorions have been formalised with the RocQ prover.

## 1 Factorions

In his book *Keys to Infinity* [2], Clifford A. Pickover dedicates one chapter to factorions: *The Loneliness of Factorions*. The definition of what it means for *n* to be a factorion depends on its representation in base 10. So, our first step is to build some basic tools to manipulate numbers and their representation in an arbitrary base *b*. The natural numbers are already equipped with the usual operations: increment *a*.+1, decrement *a*.-1, addition *a*+*b*, subtraction *a*−*b*, multiplication *a* * *b*, factoriaia *a* ‘!, power *a* ~ *b*, division *a* %/ *b*, modulo *a* %% *b* and truncated log *trunc_log* *a*. All these are standard operations maybe only the truncated log needs a bit more explanation. It is used to compute the magnitude of *n* with respect to a base *b*. One of its characteristic property is the following.

Lemma *trunc_log_eq b n k*: $1 < b \Rightarrow p \sim n \le k < p \sim n.+1 \Rightarrow \text{trunc\_log } b n = k.$

Once we have presented these operations, we can start with our formalisation. The first operation we introduce is the one that computes the *k*th digit of a number *n* in base *b*:
Definition digits b n k := (n %/ b ^ k) %% b.

We first shift the number $n$ by $k$ digits with the division and then compute the last digit using the modulo. We can derive some basic facts from this definition.

Lemma ltn_digestn b n k : 0 < b ⇒ digitn b n k < b.

Lemma digitn_exp b k l : 1 < b ⇒ digitn b (b ^ k) l = (k == l).

Lemma digitnMD b n d k : d < b ⇒ digitn b (b * m + d) n.+1 = digitn b m n.

The next notion that is formalised is the number of digits of a number $n$ in base $b$. It is defined as follows.

Definition ndigits b n := (trunc_log b n).+1.

From which, we derive some basic facts about the number of digits.

Lemma ndigits_small b n k : 1 < b ⇒ d < b ⇒ ndigits b d = 1.

Lemma ndigitsMD b n d :

$$0 < n \Rightarrow 1 < b \Rightarrow d < b \Rightarrow \text{ndigits } b \text{ (}b * n + d\text{)} = (\text{ndigits } b n\text{)} + 1.$$

Lemma ndigits_leq b n : 1 < b ⇒ 0 < n ⇒ 10 ^ (ndigits b n).-1 ≤ n.

We can then derive the decomposition theorem : $169 = 1 * 100 + 6 * 10 + 9$.

Lemma digitnE_ndigits b n : 1 < b ⇒ n = \sum_(i < ndigits b n) digitn b n i * b ^ i.

The idea of factorion is to replace the power function in the number representation with the factorial. This gives the following "factorial representation" for a number $n$.

Definition sum_fact b (n : nat) := \sum_(i < ndigits b n) (digitn b n i) '!
We can then easily derive some basic properties.

Lemma sum_fact_small b d : 1 < b ⇒ d < b ⇒ sum_fact b d = d ‘!.

Lemma sum_factMD b n d :
0 < n ⇒ 1 < b ⇒ d < b ⇒ sum_fact b (b * n + d) = d ‘! + sum_fact b n.

Then a factorion is just a number that is equal to its factorial representation
in base 10.

Definition factorion := [qualif a n | sum_fact 10 n == n].

It is easy to check that 1, 2, 145 and 40585 are factorions.

Lemma factorion1 : 1 \is a factorion.

Lemma factorion2 : 2 \is a factorion.

Lemma factorion145 : 145 \is a factorion.

Lemma factorion40585 : 40585 \is a factorion.

These are in fact the only factorions. It requires a bit more work to get this
result. The idea of the proof is first to show that a factorion can only be a
relatively small number (less than a certain bound *B*), then to exhaustively
check all the numbers less than *B*. Why there is such a bound *B* is easy to
establish. The factorial representation grows only linearly with the number
of digits : each digit contributes no more than (b − 1)! . So we get:

Lemma sum_fact_bound b n : 1 < b ⇒ sum_fact b n ≤ ndigits b n * b . -1 ‘!

We can combine this with the lower bound for a number *n* given by our
previous theorem *ndigits_leq*. So, this means that if we take a number *n* that
has more than 7 digits in base 10, its factorial representation can only be
strictly smaller than *n*.

Lemma ltn_sum_fact10 n : 7 < ndigits 10 n ⇒ sum_fact 10 n < n.

A direct corollary is then that all factorions have 7 digits or less.
Lemma factorion\_upperbound n : n \is a factorion \Rightarrow ndigits 10 n \le 7.

We are done with the first part of the proof that there are only 4 factorions.
The second part is the exploration. For this, we build a function *fact\_look\_up* that takes a relation *r* and a number of digits *m* and returns a list that contains all the numbers *k* with exactly *m* + 1 digits such that *r* holds for *k* and its factorial representation.

Fixpoint fact\_look\_up₁ (r : rel nat) (k : nat) (n p : nat) (l : seq nat) : seq N :=
  if k is k₁.+1 then
    let n₁ := 10 * n in
    let l₁ := fact\_look\_up₁ r k₁ n₁ (1 + p) l in
    let l₂ := fact\_look\_up₁ r k₁ (1 + n₁) (1 + p) l₂ in
    let l₃ := fact\_look\_up₁ r k₁ (2 + n₁) (2 + p) l₃ in
    let l₄ := fact\_look\_up₁ r k₁ (3 + n₁) (6 + p) l₄ in
    let l₅ := fact\_look\_up₁ r k₁ (4 + n₁) (24 + p) l₅ in
    let l₆ := fact\_look\_up₁ r k₁ (5 + n₁) (120 + p) l₆ in
    let l₇ := fact\_look\_up₁ r k₁ (6 + n₁) (720 + p) l₇ in
    let l₈ := fact\_look\_up₁ r k₁ (7 + n₁) (5040 + p) l₇ in
    let l₉ := fact\_look\_up₁ r k₁ (8 + n₁) (40320 + p) l₈ in
    fact\_look\_up₁ r k₁ (9 + n₁) (362880 + p) l₉
  else if (r n p) then n :: l else l.

Definition fact\_look\_up r k : seq nat :=
  let l₁ := fact\_look\_up₁ r k 1 1[::] in
  let l₂ := fact\_look\_up₁ r k 2 2 l₁ in
  let l₃ := fact\_look\_up₁ r k 3 6 l₂ in
  let l₄ := fact\_look\_up₁ r k 4 24 l₃ in
  let l₅ := fact\_look\_up₁ r k 5 120 l₄ in
  let l₆ := fact\_look\_up₁ r k 6 720 l₅ in
  let l₇ := fact\_look\_up₁ r k 7 5040 l₆ in
  let l₈ := fact\_look\_up₁ r k 8 40320 l₇ in
  fact\_look\_up₁ r k 9 362880 l₈.

Lemma fact\_look\_up\_spec (r : rel nat) m :
  0 < m \Rightarrow r m (sum\_fact 10 m) \Rightarrow m \in fact\_look\_up r (ndigits 10 m).-1.

Using this function with *r m n* = *m* == *n* and the number of digits that goes
from 0 to 7, we get the expected theorem.
Lemma factorionE n : n \is a factorion = (n \in [::1; 2; 145; 40585]).

For efficiency reason, the actual function `fact_look_up`₁ we are using computes with another type `N` equivalent to `nat` but much faster. `N` uses a binary representation of number while `nat` use an unary representation. RocQ takes 12 seconds to check this theorem.

If we look at iterations of the function `sum_fact` 10 as a graph, factorions correspond to 1-cycless. A natural extension is look at 2-cycle. There are called amical factorions in the litterature. Again, it is easy to show that 781 and 782 generate two 2-cycles.

Lemma afactorion871 : sum_fact 10 (sum_fact 10 871) = 871.

Lemma afactorion872 : sum_fact 10 (sum_fact 10 872) = 872.

Note that these two theorems are sufficient to show 871 and 872 generate 2-cycles since we know that 781 and 782 are not factorions. These 2 cycles are also distinct since 8! is greater than 1000. What about 3-cycles? These are called magical factorions. We can easy establish that 169 is a magical factorial.

Lemma mfactorion169 : sum_fact 10 (sum_fact 10 (sum_fact 10 169)) = 169.

Are there other cycles? Surprisingly there is none and we can actually formally prove that these are the only possible cycles! Again it is a brute force proof. We first prove that, when iterating the function `sum_fact` 10 starting from a number `n`, we eventually end up with a number `m` such that this number `m` is smaller than its factorial representation.

Lemma leq_sum_fact10_iter n :
    exists k, let v := iter k (sum_fact 10) n in v ≤ (sum_fact 10 v).

The proof is straightforward : when iterating we cannot always decrease because 0 is a lower bound for natural numbers. So now, we are almost done. This lemma ensures us that, when iterating starting from a number `n`,
we will eventually end up with a number *m* that is smaller than its factorial representation. If it is equal, *m* is a factorion. If it is strictly smaller, using lemma *ltn_sum_fact10*, we are sure that this number *m* has at most 7 digits. So, if we show that, if we iterate starting for any number with 7 digits or less, we always eventually end up in one of our known cycle generators, we are done. We do this using *fact_look_up_spec* with a well-chosen relation *r*. This gives our final theorem :

Lemma factorion_no_large_cycle n :
exists k, iter k (sum_fact 10) n \in [:: 1; 2; 145; 40585; 871; 872; 169].

This theorem requires more computation. Rocq takes 3 minutes to check
it. The main part of the computation is to verify that every number *b* with
at most 7 digits such that its factorial representation is greater than *n* hits
one of our generators. For this, we use a result given in [1] : all numbers less
than 10<sup>680</sup> hit a cycle in less than 60 iterations. We did not have to prove this
result. We just use 60 as the upper bound for our iterations. We compute the
list of numbers with *k* digits that does not hit one of our known generators
in 60 iterations or less. If this list is empty for *k* ≤ 7, we can conclude that
all numbers hit one of our 7 cycles.

## 2 Conclusion

This formalisation of factorion has been really a fun exercise. It mixes prov-
ing basic arithmetic fact and computing in a very nice way. The complete
formalisation is available at the following address

https://github.com/thery/mathcomp-extra/blob/master/factorion.v

References

[1] Steve Abbott. SFD chains and factorion cycles. *The Mathematical Gazette*, 88(512):261–263, 2004.

[2] Clifford A. Pickover. *Keys to Infinity*. John Wiley & Sons, 1995.