四色(22)問題 coding(99) coq(5)

四色問題は、電子計算機が数学の証明に役立つことを示した事件だった。

EVERY PLANAR MAP IS FOUR COLORABLE PART I: DISCHARGING,

K. APPEL AND W. HAKEN, 1976
https://projecteuclid.org/download/pdf_1/euclid.ijm/1256049011

参考文献は巻末に。

1. 四色問題
   新潮文庫, 2013/11, Robin Wilson/ロビン ウィルソン

https://www.amazon.co.jp/dp/4102184619/ https://bookmeter.com/books/7667829 https://booklog.jp/item/1/4102184619

近代に説かれた数学の未解決問題の解決に関連する成果として、ヨシオ　シマモトという人が、シマモトの馬蹄形という問題を提起し、Ｄ可約性を課題とする環の大きさが１４の配置に関する課題があったということを知りました。
また、コンピュータを使って証明されたことが、検証の妥当性に疑問や懐疑を投げかけられたということを、この本で初めて知りました。
「コンピュータは疲れを知らない」反面、電磁的な不具合があった際に、検出可能であることが証明されていない場合があるかもしれません。
いずれにしても、四色問題という数学的にしか価値がないような問題を、一部の数学者による批評では美しい数学的手法ではない方法で解決されたということが、数学のおもしろさと、コンピュータのおもしろさを知るきっかけになるかもしれない。

40年後に、Microsoftの技術者が、coq でffreflectの拡張をして証明したことは著名。
https://github.com/math-comp/fourcolor/tree/master/theories

<この項は書きかけです。順次追記します。>

A computer-checked proof of the Four Colour Theorem

Georges Gonthier, Microsoft Research Cambridge, 2005
ssreflectなどの資料がリンク切れがあり、現在調査中。

Formal Proof—The Four- Color Theorem Georges Gonthier
http://cs.ru.nl/~freek/courses/tt-2014/read/tx081101382p.pdf

p4

   Variable R : real_model.
      Theorem four_color : (m : (map R))
        (simple_map m) -> (map_colorable (4) m).
      Proof.
Exact (compactness_extension four_color_finite). Qed.

p6

Theorem four_color_hypermap : (g : hypermap) (planar_bridgeless g) -> (four_colorable g).

p12

 Variable cf : config.
 Definition check_reducible : bool := ...
 Definition cfreducible : Prop := ...
 Lemma check_reducible_valid : check_reducible -> cfreducible.

p12a

Lemma cfred232 : (cfreducible (Config 11 33 37
           H 2 H 13 Y 5 H 10 H 1 H 1 Y 3 H 11 Y 4 H
           9 H 1 Y 3 H 9 Y 6 Y 1 Y 1 Y 3 Y 1 Y Y 1 Y)).

ss reflect

参考文献の参考文献

EVERY PLANAR MAP IS FOUR COLORABLE PART I: DISCHARGING, BIBLIOGRAPHY

1. F.ALLAIRE,Aminimal5-chromaticplanargraphcontainsa6-valentvertex,toappear.
2. F. ALLAIRE AND E. R. SWART, Z systematic approach to the determination ofreducible configurations in the four-color conjecture, J. Combinatorial Theory (B), to appear.
3. K. APPEL AND W. HAKEN, An unavoidable set of configurations in planar triangulations, J. Combinatorial Theory (B), to appear.
4. K. APPEL AND W. HAKEN,The existence ofunavoidable sets #eo#raphically good configurations, Illinois J. of
   Math., vol. 20 (1976), pp. 218-297. 5.K.APPEL,W.HAKEN,ANDJ.MAYER,Triangulations vs dpars dans le probleme des quatre couleurs, J. Combinatorial Theory (B), to appear.
   6.A. BERnART, Six rings in minimal five color maps, Amer. J. Math., vol. 69 (1947), pp. , 391-412.
   7.A. BERnART,Another reducible edge configuration, Amer. J. Math., vol. 70 (1948), pp. 144-146.
   8.F. BERI-IART, On the characterization of reductions of small order, J. CombinatorialTheory (B), to appear.
   9.F.BERNHARTAND S.GILL,Anex tension of Winn’s result on reducibleminorneighborhoods, to appear.
   10 .G. D. BIRKHOr, The reducibility ofmaps, Amer. J. Math., vol. 35 (1913), pp. 114--128.
5. C. CHOJNACKI, A contribution to the four color problem, Amer. J. Math., vol. 64 (1942),
   pp. 36--54.
   12.K. D2RRE, Untersuchun#en an Men#en yon Si#nierunyen, Doctoral Dissertation, Technische Universitit Hannover, 1969.
6. P. ERRERA, Une contribution au probldme des quatre couleurs, Bull. Soc. Math. France, vol. 53 (1925), pp. 42-55.
7. PH.FRArILIN,The four color problem, Amer.J.Math.,vol.44(1922),pp.225-236.
8. W.HA:N,Anex is tence theorem for planar maps, J.Combinatorial Theory,vol.14(1973), pp. 180-184.
   16.H. HEESCH, Untersuchungen zum Vierfarbenproblem, B-I-Hochschulscripten 810/810a/ , 810b, Bibliographisches Institut, Mannheim/Vienna/Zurich, 1969.
   17.H. HEESCH, Chromatic reduction the triangulations T, e e + eT, J. Combinatorial of Theory, vol. 13 (1972), pp. 46-53.

A computer-checked proof of the Four Colour Theorem

Rerefences

1. S. B. Akers, ‘Binary Decision Diagrams’, IEEE Transactions on Computers c- 27(6) (1978), 509–16.
2. T. Altenkirch, ‘Constructions, Inductive types and Strong Normalization’, PhD Thesis, University of Edinburgh, 1993.
3. K. Appel and W. Haken, ‘Every map is four colourable’, Bulletin of the American Mathematical Society 82 (1976), 711–12.
4. K. Appel and W. Haken, ‘Every map is four colourable, Part I: Discharging’, Illinois Journal of Mathematics 21 (1977), 429–90.
5. K. Appel and W. Haken, ‘Every map is four colourable, Part II: Reducibility’, Illinois Journal of Mathematics 21 (1977), 491–567.
6. K. Appel and W. Haken, Every map is four colourable, American Mathematical Society, 1989.
7. D. Aspinall, ‘Proof General: A Generic Tool for Proof Development’,
   Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, (TACAS) 2000, Springer-Verlag LNCS 1785, 2000.
8. G. Barthe, J. Hatcliff and M.H. Sørensen, ‘CPS translations and applications: the Cube and beyond’, Higher Order and Symbolic Computation 12(2) (1999), 125– 70.
9. Y . Bertot and P . Castéran, Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Construction, Texts in Theoretical Computer Science, an EATCS series. Springer Verlag, 2004.
10. G. D. Birkhoff, ‘The reducibility of maps’, American Journal of Mathematics 35 (1913), 115–28.
11. S. Boutin, ‘Using reflection to build efficient and certified decision procedures’, Proceedings of Theorethical Aspects of Computer Science (TACS) 1997, Springer- Verlag LNCS 1281, 1997.
12. R. E. Bryant, ‘Graph-Based Algorithms for Boolean Function Manipulation’, IEEE Transactions on Computers c-35(8) (1986), 677–91.
13. The Coq Development Team, ‘The Coq reference manual, version 7.3.1’, system and documentation available from ftp://ftp.inria.fr/INRIA/coq/V.7.3.1.
14. T. Coquand and G. Huet, ‘The Calculus of Constructions’, Information and Computation 76(2/3) (1988), 95–120.
15. R. Cori, ‘Un code pour les graphes planaires et ses applications’ Astérisque 27 (1975), 169.
16. R. Cori and A. Machí, ‘Maps, hypermaps and their automorphisms: a survey I, II, III’, Expositiones Mathematicae 10(5) (1992), 403–67.
17. H. Geuvers, R. Pollack, F. Wiedijk and J. Zwanenburg, ‘A Constructive Algebraic Hierarchy in Coq’, Journal of Symbolic Computation 34(4) (2002) 271–86.
18. H. Heesch, Untersuchungen zum Vierfarbenproblem, 810/a/b, Bibliographishes Institut, Mannheim-Wien-Zürich, 1969.
    19.M. Hofmann and T. Streicher, ‘The groupoid interpretation of type theory’, Proceedings of Twenty-five years of constructive type theory, Oxford University Press, 1998.
19. J. E. Hopcroft and R. E. Tarjan, ‘Efficient planarity testing’, Journal of the Association for Computer Machinery 21 (1974), 145–54.
20. G. Huet, ‘The Zipper’, Journal of Functional Programming 7(5) (1997), 549–54. 22. A. B. Kempe, ‘On the geographical problem of the four colours’, American
    Journal of Mathematics 2 (part 3) (1879), 193–200.
21. K. Kuratowski, ‘Sur le problème des courbes gauches en topologie’, Fundamenta
    Mathematicae 15 (1930), 271–83.
22. A. Miquel, ‘A Model for Impredicative Type Systems, Universes, Intersection
    Types and Subtyping’, Proceedings of the fifteenth annual IEEE symposium on
    Logic in Computer Science (2000).
23. M. H. A. Newman, Elements of the topology of plane sets of points, Dover
    Publications (1992).
    26.N. Robertson, D. Sanders, P. Seymour, and R. Thomas. ‘The Four-Colour
    Theorem’, Journal Combinatorial Theory, Series B 70 (1997), 2–44.
24. N. Robertson, D. Sanders, P. Seymour, and R. Thomas. ‘Discharging Cartwheels’, unpublished manuscript, available at
    ftp://ftp.math.gatech.edu/pub/users/thomas/fcdir/discharge.ps.
25. T. L. Saaty and P. C. Kainen, The Four-Colour Problem: Assaults and Conquest,
    McGraw-Hill, 1977.
26. S. Stahl, ‘A Combinatorial Analog of the Jordan Curve Theorem’, Journal of
    Combinatorial Theory, Series B 35 (1983), 28–38.
27. P. G. Tait, ‘Note on a theorem in the geometry of position’, Transactions of the Royal Society of Edinburgh 29 (1880), 657–60.
28. W. Tutte, ‘Duality and trinity’, Colloquium Mathematical Society Janos Bolyai 10 (1975) 1459–72.
29. W. T. Tutte, ‘Combinatorial oriented maps’, Canadian Journal of Mathematics 31 (1979), 986–1004.
30. T. R. S. Walsh, ‘Hypermaps versus bipartite maps’, Journal of Combinatorial Theory, Series B 18 (1975) 155–63.
31. D. W. Walkup, ‘How many ways can a permutation be factored into two n- cycles?’, Discrete Mathematics 28 (1979), 315–19.
32. B. Werner, ‘Une Théorie des Constructions Inductives’, PhD Thesis, Université Paris VII, 1994.
33. R. Wilson, Four Colours Suffice, Penguin books, 2002.

岩波数学辞典　四色問題　参考文献

［1］T. R. Jensen - B. Toft, Graph coloring　problems, Wiley, 1995
［2］K. Appel - W. Haken,　Every planar map is four colorable I, discharging,
Illinois J. Math., 21(1977), 429-490
［3］K. Appel　- W. Haken - J. Koch, Every planar map is four　colorable II, reducibility, Illinois J. Math., 21　(1977), 491-567
［4］Proc. London Math. Soc.,　9(1878), 148
［5］P. Franklin, A six color problem,　J. Math. Phys., 13(1934), 363-369
［6］P. J.　Heawood, Map-colour theorems, Quart. J. Math.,　24(1890), 332-338
［7］H. Heesch, Untersuchungen　zum Vierfarbenproblem, Bibliog. Institut, AG,
Mannheim, 1969
［8］A. B. Kempe, On the　geographical problem of the four-colors, Amer.
J. Math., 2(1879), 193-200
［9］G. Ringel - J.W.　T. Youngs, Solution of the Heawood map coloring　problem, Proc. Nat. Acad. Sci. USA, 60(1968)　438-445
［10］N. Robertson - D. Sanders - P.　Seymour - R. Thomas, The four-colour theorem,　J. Comb. Theory Ser. B, 70(1997), 2-44
［11］P. G. Tait, Remarks on the colouring of maps,　Proc. Roy. Soc. Edinburgh, 10(1880), 729
［12］C.　Thomassen, Every planar graph is 5-choosable, J.　Comb. Theory Ser. B, 62(1994), 180-181
［13］M.　Voigt, List colourings of planar graphs, Discrete　Math., 120(1993), 215-219.

参考文献

Proof Engineering, from the Four Colour to the Odd Order Theorem
https://www.youtube.com/watch?v=d-oV0fs3e6s

The Mathematical Components library
https://github.com/math-comp/math-comp/releases

SSReflect
https://www.math.nagoya-u.ac.jp/~garrigue/lecture/2015_AW/coq9.pdf

Coq/SSreflect を用いた 条件付独立性の形式化について
http://www.math.s.chiba-u.ac.jp/report/files/17001.pdf

一覧

物理記事　上位100
https://qiita.com/kaizen_nagoya/items/66e90fe31fbe3facc6ff

量子(0) 計算機, 量子力学
https://qiita.com/kaizen_nagoya/items/1cd954cb0eed92879fd4

数学関連記事１００
https://qiita.com/kaizen_nagoya/items/d8dadb49a6397e854c6d

言語・文学記事　１００
https://qiita.com/kaizen_nagoya/items/42d58d5ef7fb53c407d6

医工連携関連記事一覧
https://qiita.com/kaizen_nagoya/items/6ab51c12ba51bc260a82

自動車　記事　１００
https://qiita.com/kaizen_nagoya/items/f7f0b9ab36569ad409c5

通信記事１００
https://qiita.com/kaizen_nagoya/items/1d67de5e1cd207b05ef7

日本語（０）一欄
https://qiita.com/kaizen_nagoya/items/7498dcfa3a9ba7fd1e68

英語(0) 一覧
https://qiita.com/kaizen_nagoya/items/680e3f5cbf9430486c7d

転職(0)一覧
https://qiita.com/kaizen_nagoya/items/f77520d378d33451d6fe

仮説（0）一覧（目標100現在40）
https://qiita.com/kaizen_nagoya/items/f000506fe1837b3590df

Qiita(0)Qiita関連記事一覧（自分）
https://qiita.com/kaizen_nagoya/items/58db5fbf036b28e9dfa6

鉄道（０）鉄道のシステム考察はてっちゃんがてつだってくれる
https://qiita.com/kaizen_nagoya/items/26bda595f341a27901a0

安全（0）安全工学シンポジウムに向けて: 21
https://qiita.com/kaizen_nagoya/items/c5d78f3def8195cb2409

一覧の一覧( The directory of directories of mine.) Qiita(100)
https://qiita.com/kaizen_nagoya/items/7eb0e006543886138f39

Ethernet 記事一覧　Ethernet(0)
https://qiita.com/kaizen_nagoya/items/88d35e99f74aefc98794

Wireshark 一覧 wireshark(0)、Ethernet(48)
https://qiita.com/kaizen_nagoya/items/fbed841f61875c4731d0

線網（Wi-Fi）空中線(antenna)(0) 記事一覧(118/300目標)
https://qiita.com/kaizen_nagoya/items/5e5464ac2b24bd4cd001

OSEK OS設計の基礎　OSEK(100)
https://qiita.com/kaizen_nagoya/items/7528a22a14242d2d58a3

Error一覧 error(0)
https://qiita.com/kaizen_nagoya/items/48b6cbc8d68eae2c42b8

プログラマによる、プログラマのための、統計(0)と確率のプログラミングとその後
https://qiita.com/kaizen_nagoya/items/6e9897eb641268766909

官公庁・学校・公的団体（NPOを含む）システムの課題、官（０）
https://qiita.com/kaizen_nagoya/items/04ee6eaf7ec13d3af4c3

「はじめての」シリーズ　 ベクタージャパン　
https://qiita.com/kaizen_nagoya/items/2e41634f6e21a3cf74eb

AUTOSAR(0)Qiita記事一覧, OSEK(75)
https://qiita.com/kaizen_nagoya/items/89c07961b59a8754c869

プログラマが知っていると良い「公序良俗」
https://qiita.com/kaizen_nagoya/items/9fe7c0dfac2fbd77a945

LaTeX(0) 一覧　
https://qiita.com/kaizen_nagoya/items/e3f7dafacab58c499792

自動制御、制御工学一覧（０）
https://qiita.com/kaizen_nagoya/items/7767a4e19a6ae1479e6b

Rust(0) 一覧　
https://qiita.com/kaizen_nagoya/items/5e8bb080ba6ca0281927

小川清最終講義、最終講義（再）計画, Ethernet(100) 英語(100) 安全(100)
https://qiita.com/kaizen_nagoya/items/e2df642e3951e35e6a53

＜この記事は個人の過去の経験に基づく個人の感想です。現在所属する組織、業務とは関係がありません。＞
This article is an individual impression based on the individual's experience. It has nothing to do with the organization or business to which I currently belong.
＜この記事は個人の過去の経験に基づく個人の感想です。現在所属する組織、業務とは関係がありません。＞

文書履歴(document history)

ver. 0.01 初稿 20190108
ver. 0.02 岩波数学辞典　参考文献追記 20190109
ver. 0.03 ありがとう追記 　 20230522

最後までおよみいただきありがとうございました。

いいね　💚、フォローをお願いします。

Thank you very much for reading to the last sentence.

Please press the like icon 💚　and follow me for your happy life.