axio/index.html at main · groupoid/axio · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
<!DOCTYPE html><html><head><meta charset="utf-8"><meta http-equiv="x-ua-compatible" content="ie=edge"><meta property="fb:app_id" content="118554188236439"><meta name="viewport" content="width=device-width, initial-scale=1"><meta name="author" content="Maxim Sokhatsky"><meta name="twitter:site" content="@5HT"><meta name="twitter:creator" content="@5HT"><meta property="og:type" content="website"><meta property="og:image" content="https://avatars.githubusercontent.com/u/17128096?s=400&amp;u=66a63d4cdd9625b2b4b37d724cc00fe6401e5bd8&amp;v=4"><meta name="msapplication-TileColor" content="#ffffff"><meta name="msapplication-TileImage" content="https://anders.groupoid.space/images/ms-icon-144x144.png"><meta name="theme-color" content="#ffffff"><link rel="stylesheet" href="https://anders.groupoid.space/main.css?v=1"><link rel="apple-touch-icon" sizes="57x57" href="https://anders.groupoid.space/images/apple-icon-57x57.png"><link rel="apple-touch-icon" sizes="60x60" href="https://anders.groupoid.space/images/apple-icon-60x60.png"><link rel="apple-touch-icon" sizes="72x72" href="https://anders.groupoid.space/images/apple-icon-72x72.png"><link rel="apple-touch-icon" sizes="76x76" href="https://anders.groupoid.space/images/apple-icon-76x76.png"><link rel="apple-touch-icon" sizes="114x114" href="https://anders.groupoid.space/images/apple-icon-114x114.png"><link rel="apple-touch-icon" sizes="120x120" href="https://anders.groupoid.space/images/apple-icon-120x120.png"><link rel="apple-touch-icon" sizes="144x144" href="https://anders.groupoid.space/images/apple-icon-144x144.png"><link rel="apple-touch-icon" sizes="152x152" href="https://anders.groupoid.space/images/apple-icon-152x152.png"><link rel="apple-touch-icon" sizes="180x180" href="https://anders.groupoid.space/images//apple-icon-180x180.png"><link rel="icon" type="image/png" sizes="192x192" href="https://anders.groupoid.space/images/android-icon-192x192.png"><link rel="icon" type="image/png" sizes="32x32" href="https://anders.groupoid.space/images/favicon-32x32.png"><link rel="icon" type="image/png" sizes="96x96" href="https://anders.groupoid.space/images/favicon-96x96.png"><link rel="icon" type="image/png" sizes="16x16" href="https://anders.groupoid.space/images/favicon-16x16.png"><link rel="manifest" href="https://anders.groupoid.space/images/manifest.json"><style>p {font-size: 16px}
svg a{fill:blue;stroke:blue}
[data-mml-node="merror"]>g{fill:red;stroke:red}
[data-mml-node="merror"]>rect[data-background]{fill:yellow;stroke:none}
[data-frame],[data-line]{stroke-width:70px;fill:none}
.mjx-dashed{stroke-dasharray:140}
.mjx-dotted{stroke-linecap:round;stroke-dasharray:0,140}
use[data-c]{stroke-width:3px}
</style></head><body class="content"></body></html><html><head><meta property="og:title" content="AXIO/1"><meta property="og:description" content="FORMAL MATHEMATICS"><meta property="og:url" content="https://groupoid.github.io/axio/"></head></html><title>AXIO/1</title><header class="header"><div class="header__titles"><h1 class="header__title">AXIO/1</h1><h4 class="header__subtitle">Формальне середовище виконання, система вищих мов та базові бібліотеки для програмування, доведення теорем і формальної філософії</h4></div></header><article class="main"><div class="om"><section><h1>АНОТАЦІЯ</h1></section><aside>Дисертація на здобуття ступеня <br> доктора філософії <br> Максима Сохацького<time>1 Вересня 2021</time></aside><p style="font-size: 14px;">Дисертація присвячена розробці першої формальної системи AXIO/1,
яка встановлює новаторський підхід до математичної верифікації та
створює уніфіковану систему формальних мов для програмування, математик та філософій.
У процесі створення цієї системи автор проаналізував синтаксис і семантику понад 50 мов програмування
з промислових та академічних доменів, реалізувавши 8 власних мов.
Робота презентує концептуальну модель уніфікованої мовної системи, що складається з 8 математичних мов,
та демонструє їхні імплементації. Основна мета — синтез універсальної платформи для механічної
верифікації теорем, що охоплює класичні та синтетичні математики в обчислювально перевірюваному формалізмі.
</p><p style="font-size: 14px;">Перша формальна система AXIO/1 визначає формальний підхід до математичної
верифікації та описує спробу автора у цій парадигмі побудувати
уніфіковану систему формальних мов для програмування,
математики та філософії. В процесі розробки моделі такої
системи автору довелося апробувати підхід та практики
для головних функціональних формальних академічних мов.
</p><section><h1>СТРУКТУРА РОБОТИ</h1></section><p>Мови розглядаються як моноїдальні категорії,
де об’єкти — простори програм, а морфізми — правила верифікації та компіляції.
Система розкладається на спектральну послідовність мов, індексовану натуральними числами.</p><p>Як результат дослідження пропонується унікальна відкрита система, яка інтегрує:
1) системне програмне забезпечення: модального середовища виконання разом з інтерпретатором написаним на формальній мові;
2) бібліотеки: для прикладного програмування в середовищах виконання;
3) прикладне програмне забезпечення: системи вищих формальних мов з різними ефективними моделями для різних математик та їх імплементаціями;
4) математичні бібліотеки: механізовані теореми для верифікації.</p><p>Робота черпає натхнення з LISP-машин, APL-систем, ранніх систем доведення теорем (як AUTOMATH),
віртуальних машин для паралельної обробки (як BEAM) та кубічних систем (HTS).
</p></div><h2>Середовище виконання</h2><p>Середовища виконання — зерна.</p><div class="index"><div class="index__col"><h2>Зерна</h2><ul><li><a href="https://alonzo.groupoid.space/">ДЗК-інтерпретатор</a></li><li><a href="https://yves.groupoid.space/">СМК-інтерпретатор</a></li></ul></div><div class="index__col"><h2>Бібліотека</h2><ul><li><a href="https://anders.groupoid.space/foundations/modal/process/">Процеси</a></li><li><a href="https://groupoid.space/runtime/effects/">Ефекти</a></li><li><a href="https://anders.groupoid.space/foundations/mltt/io/">IO</a></li><li><a href="https://anders.groupoid.space/foundations/mltt/ioi/">IOI</a></li></ul></div></div><h2>Мови програмування</h2><p>Мови програмування — паростки.</p><div class="index"><div class="index__col"><h2>Паростки</h2><ul><li><a href="https://henk.groupoid.space">Ядро розшарування</a></li><li><a href="https://per.groupoid.space">Ядро локальних ДЗК</a></li><li><a href="https://christine.groupoid.space">Індуктивне ядро</a></li><li><a href="https://anders.groupoid.space/">Гомотопічне ядро</a></li><li><a href="https://laurent.groupoid.space">Ядро аналізу</a></li><li><a href="https://dan.groupoid.space">Сімліціальне ядро</a></li><li><a href="https://jack.groupoid.space">K-теоретичне ядро</a></li><li><a href="https://urs.groupoid.space">Супергеометричне ядро</a></li></ul></div><div class="index__col"><h2>Бібліотеки</h2><ul><li><a href="https://groupoid.space/misc/library/">Математичні компоненти</a></li><li><a href="https://groupoid.space/institute/КМ-111/10-Гомотопічна-теорія-типів/">Курс по теорії типів</a></li><li><a href="https://groupoid.space/misc/internship/">Інтернатура</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/hopf/">Розшарування хопфа</a></li><li><a href="https://groupoid.space/">Групоїд Інфініті</a></li></ul></div></div><h2>Формалізація математик</h2><p>Математичні теорії — дерева, математики — їх ліси.</p><div class="index"><div class="index__col"><h2><b>ANALYSIS</b></h2><ul><li><a href='https://anders.groupoid.space/mathematics/analysis/topology/'>TOPOLOGY</a></li><li><a href='https://anders.groupoid.space/mathematics/analysis/set/'>SET</a></li><li><a href='https://anders.groupoid.space/mathematics/analysis/rational/'>ℚ</a>, <a href='https://anders.groupoid.space/mathematics/analysis/real/'>ℝ</a>, <a href='https://anders.groupoid.space/mathematics/analysis/complex/'>ℂ</a>, <a href='https://anders.groupoid.space/mathematics/analysis/quatro/'>ℍ</a>, <a href='https://anders.groupoid.space/mathematics/analysis/octo/'>𝕆</a></li></ul></div><div class="index__col"><h2><b>ALGEBRA</b></h2><ul><li><a href="https://anders.groupoid.space/mathematics/algebra/group/">GROUP</a></li><li><a href="https://anders.groupoid.space/mathematics/algebra/algebra/">ALGEBRA</a></li><li><a href="https://anders.groupoid.space/mathematics/algebra/homology/">HOMOLOGY</a></li></ul></div><div class="index__col"><h2><b>GEOMETRY</b></h2><ul><li><a href="https://anders.groupoid.space/mathematics/geometry/etale/">ETALE</a></li><li><a href="https://anders.groupoid.space/mathematics/geometry/bundle/">BUNDLE</a></li><li><a href="https://anders.groupoid.space/mathematics/geometry/manifold/">MANIFOLD</a></li><li><a href="https://anders.groupoid.space/mathematics/geometry/derham/">DE RHAM</a></li></ul></div><div class="index__col"><h2><b>HOMOTOPY</b></h2><ul><li><a href="https://anders.groupoid.space/mathematics/homotopy/coequalizer/">COEQUALIZER</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/pushout/">PUSHOUT</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/pullback/">PULLBACK</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/hopf/">HOPF</a></li><li><a href="https://anders.groupoid.space/mathematics/homotopy/cw/">CW</a></li></ul></div><div class="index__col"><h2><b>CATEGORIES</b></h2><ul><li><a href="https://anders.groupoid.space/mathematics/categories/category/">CATEGORY</a></li><li><a href="https://anders.groupoid.space/mathematics/categories/functor/">FUNCTOR</a></li><li><a href="https://anders.groupoid.space/mathematics/categories/groupoid/">GROUPOID</a></li><li><a href="https://anders.groupoid.space/mathematics/categories/topos/">TOPOS</a></li><li><a href="https://anders.groupoid.space/mathematics/categories/presheaf/">PRESHEAF</a></li></ul></div></div><div class="om"><section><h1>Середовище виконання</h1></section><p>Розділ присвячений загальній таксономії мов програмування. Виявляється, що
всі мови програмування так чи інакше є внутрішніми мовами категорій, що містять структуру
декартово-замкнених або симетричних моноїдальних категорій. Кінцева мета — створення
<a href="https://groupoid.github.io/languages/">енциклопедії мов програмування</a> і
<a href="https://o83.github.io/platform.rs/">прототипу обчислювального середовища</a>.
</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.011ex;" xmlns="http://www.w3.org/2000/svg" width="7.891ex" height="1.59ex" role="img" focusable="false" viewBox="0 -698 3488 703" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1-TEX-B-1D400" d="M296 0Q278 3 164 3Q58 3 49 0H40V62H92Q144 62 144 64Q388 682 397 689Q403 698 434 698Q463 698 471 689Q475 686 538 530T663 218L724 64Q724 62 776 62H828V0H817Q796 3 658 3Q509 3 485 0H472V62H517Q561 62 561 63L517 175H262L240 120Q218 65 217 64Q217 62 261 62H306V0H296ZM390 237L492 238L440 365Q390 491 388 491Q287 239 287 237H390Z"></path><path id="MJX-1-TEX-B-1D425" d="M43 686L134 690Q225 694 226 694H232V62H301V0H292Q274 3 170 3Q67 3 49 0H40V62H109V332Q109 387 109 453T110 534Q110 593 108 605T94 620Q80 624 53 624H40V686H43Z"></path><path id="MJX-1-TEX-B-1D428" d="M287 -5Q228 -5 182 10T109 48T63 102T39 161T32 219Q32 272 50 314T94 382T154 423T214 446T265 452H279Q319 452 326 451Q428 439 485 376T542 221Q542 156 514 108T442 33Q384 -5 287 -5ZM399 230V250Q399 280 398 298T391 338T372 372T338 392T282 401Q241 401 212 380Q190 363 183 334T175 230Q175 202 175 189T177 153T183 118T195 91T215 68T245 56T287 50Q348 50 374 84Q388 101 393 132T399 230Z"></path><path id="MJX-1-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-1-TEX-B-1D433" d="M48 262Q48 264 54 349T60 436V444H252Q289 444 336 444T394 445Q441 445 450 441T459 418Q459 406 458 404Q456 399 327 229T194 55H237Q260 56 268 56T297 58T325 65T348 77T370 98T384 128T395 170Q400 197 400 216Q400 217 431 217H462V211Q461 208 453 108T444 6V0H245Q46 0 43 2Q32 7 32 28V33Q32 41 40 52T84 112Q129 170 164 217L298 393H256Q189 392 165 380Q124 360 115 303Q110 280 110 256Q110 254 79 254H48V262Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D400" xlink:href="#MJX-1-TEX-B-1D400"></use><use data-c="1D425" xlink:href="#MJX-1-TEX-B-1D425" transform="translate(869,0)"></use><use data-c="1D428" xlink:href="#MJX-1-TEX-B-1D428" transform="translate(1188,0)"></use><use data-c="1D427" xlink:href="#MJX-1-TEX-B-1D427" transform="translate(1763,0)"></use><use data-c="1D433" xlink:href="#MJX-1-TEX-B-1D433" transform="translate(2402,0)"></use><use data-c="1D428" xlink:href="#MJX-1-TEX-B-1D428" transform="translate(2913,0)"></use></g></g></g></g></svg></mjx-container> — мінімальна мова для послідовних обчислень в декартово-замкнених категоріях.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="5.559ex" height="1.566ex" role="img" focusable="false" viewBox="0 -686 2457 692" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-2-TEX-B-1D418" d="M605 0Q581 3 434 3Q286 3 262 0H250V62H358V275L126 624H19V686H30Q54 683 189 683Q361 685 370 686H383V624H308L319 608Q330 591 353 556T396 491L484 359L660 623Q660 624 623 624H585V686H595Q613 683 728 683Q832 683 841 686H849V624H742L509 274V62H618V0H605Z"></path><path id="MJX-2-TEX-B-1D42F" d="M401 444Q413 441 495 441Q568 441 574 444H580V382H510L409 156Q348 18 339 6Q331 -4 320 -4Q318 -4 313 -4T303 -3H288Q273 -3 264 12T221 102Q206 135 197 156L96 382H26V444H34Q49 441 145 441Q252 441 270 444H279V382H231L284 264Q335 149 338 149Q338 150 389 264T442 381Q442 382 418 382H394V444H401Z"></path><path id="MJX-2-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-2-TEX-B-1D42C" d="M38 315Q38 339 45 360T70 404T127 440T223 453Q273 453 320 436L338 445L357 453H366Q380 453 383 447T386 403V387V355Q386 331 383 326T365 321H355H349Q333 321 329 324T324 341Q317 406 224 406H216Q123 406 123 353Q123 334 143 321T188 304T244 294T285 286Q305 281 325 273T373 237T412 172Q414 162 414 142Q414 -6 230 -6Q154 -6 117 22L68 -6H58Q44 -6 41 0T38 42V73Q38 85 38 101T37 122Q37 144 42 148T68 153H75Q87 153 91 151T97 147T103 132Q131 46 220 46H230Q257 46 265 47Q330 58 330 108Q330 127 316 142Q300 156 284 162Q271 168 212 178T122 202Q38 243 38 315Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D418" xlink:href="#MJX-2-TEX-B-1D418"></use><use data-c="1D42F" xlink:href="#MJX-2-TEX-B-1D42F" transform="translate(869,0)"></use><use data-c="1D41E" xlink:href="#MJX-2-TEX-B-1D41E" transform="translate(1476,0)"></use><use data-c="1D42C" xlink:href="#MJX-2-TEX-B-1D42C" transform="translate(2003,0)"></use></g></g></g></g></svg></mjx-container> — мінімальна мова для паралельних обчислень в симетричних моноїдальних категоріях.</p><p>Повний перелік інтерпретаторів і асемблерів, як цілей компіляцій, представлений в роботі:
1) інтерпретатор MinCaml написаний на MinCaml;
2) авторський лінивий лямбда інтерпретатор з паралельним середовищем виконанням без надлишкового копіювання,
   AVX-512 векторизацією і чергах на CAS-курсорах на мові програмування Rust;
3) віртуальна машина BEAM мови програмування Erlang від Ericsson (LING).
4) Intel асемблер як ціль компіляції для MinCaml;
5) ARM64 асемблер як ціль компіляції для MinCaml.
</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.025ex;" xmlns="http://www.w3.org/2000/svg" width="3.837ex" height="1.577ex" role="img" focusable="false" viewBox="0 -686 1696 697" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-3-TEX-B-1D409" d="M174 114Q174 96 169 82T159 63T144 47L155 45Q183 40 203 40Q271 40 290 104Q294 118 294 150T295 380V624H154V686H169Q196 683 365 683Q499 683 517 686H527V624H446V379Q446 183 446 153T441 108Q413 32 315 2Q266 -11 208 -11Q160 -11 118 -2T42 37T8 114V122Q8 150 30 174T91 198T152 174T174 122V114Z"></path><path id="MJX-3-TEX-B-1D428" d="M287 -5Q228 -5 182 10T109 48T63 102T39 161T32 219Q32 272 50 314T94 382T154 423T214 446T265 452H279Q319 452 326 451Q428 439 485 376T542 221Q542 156 514 108T442 33Q384 -5 287 -5ZM399 230V250Q399 280 398 298T391 338T372 372T338 392T282 401Q241 401 212 380Q190 363 183 334T175 230Q175 202 175 189T177 153T183 118T195 91T215 68T245 56T287 50Q348 50 374 84Q388 101 393 132T399 230Z"></path><path id="MJX-3-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D409" xlink:href="#MJX-3-TEX-B-1D409"></use><use data-c="1D428" xlink:href="#MJX-3-TEX-B-1D428" transform="translate(594,0)"></use><use data-c="1D41E" xlink:href="#MJX-3-TEX-B-1D41E" transform="translate(1169,0)"></use></g></g></g></g></svg></mjx-container> — українська віртуальна машина Джо Армстронга.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="6.421ex" height="1.586ex" role="img" focusable="false" viewBox="0 -695 2838 701" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-4-TEX-B-1D40B" d="M643 285Q641 280 629 148T612 4V0H39V62H147V624H39V686H51Q75 683 228 683Q415 685 425 686H439V624H304V62H352H378Q492 62 539 138Q551 156 558 178T569 214T576 255T581 289H643V285Z"></path><path id="MJX-4-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-4-TEX-B-1D42C" d="M38 315Q38 339 45 360T70 404T127 440T223 453Q273 453 320 436L338 445L357 453H366Q380 453 383 447T386 403V387V355Q386 331 383 326T365 321H355H349Q333 321 329 324T324 341Q317 406 224 406H216Q123 406 123 353Q123 334 143 321T188 304T244 294T285 286Q305 281 325 273T373 237T412 172Q414 162 414 142Q414 -6 230 -6Q154 -6 117 22L68 -6H58Q44 -6 41 0T38 42V73Q38 85 38 101T37 122Q37 144 42 148T68 153H75Q87 153 91 151T97 147T103 132Q131 46 220 46H230Q257 46 265 47Q330 58 330 108Q330 127 316 142Q300 156 284 162Q271 168 212 178T122 202Q38 243 38 315Z"></path><path id="MJX-4-TEX-B-1D425" d="M43 686L134 690Q225 694 226 694H232V62H301V0H292Q274 3 170 3Q67 3 49 0H40V62H109V332Q109 387 109 453T110 534Q110 593 108 605T94 620Q80 624 53 624H40V686H43Z"></path><path id="MJX-4-TEX-B-1D422" d="M72 610Q72 649 98 672T159 695Q193 693 217 670T241 610Q241 572 217 549T157 525Q120 525 96 548T72 610ZM46 442L136 446L226 450H232V62H294V0H286Q271 3 171 3Q67 3 49 0H40V62H109V209Q109 358 108 362Q103 380 55 380H43V442H46Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D40B" xlink:href="#MJX-4-TEX-B-1D40B"></use><use data-c="1D41E" xlink:href="#MJX-4-TEX-B-1D41E" transform="translate(692,0)"></use><use data-c="1D42C" xlink:href="#MJX-4-TEX-B-1D42C" transform="translate(1219,0)"></use><use data-c="1D425" xlink:href="#MJX-4-TEX-B-1D425" transform="translate(1673,0)"></use><use data-c="1D422" xlink:href="#MJX-4-TEX-B-1D422" transform="translate(1992,0)"></use><use data-c="1D41E" xlink:href="#MJX-4-TEX-B-1D41E" transform="translate(2311,0)"></use></g></g></g></g></svg></mjx-container> — верифікатор TLA+ протоколів Леслі Лампорта.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: 0;" xmlns="http://www.w3.org/2000/svg" width="4.699ex" height="1.572ex" role="img" focusable="false" viewBox="0 -695 2077 695" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-5-TEX-B-1D413" d="M41 425Q41 426 51 545T62 669V675H737V669Q738 665 748 546T758 425V419H696V425Q687 517 669 555T595 607Q578 612 522 613H478V62H631V0H615Q585 3 399 3Q214 3 184 0H168V62H321V613H277H263Q164 613 134 561Q113 527 103 425V419H41V425Z"></path><path id="MJX-5-TEX-B-1D422" d="M72 610Q72 649 98 672T159 695Q193 693 217 670T241 610Q241 572 217 549T157 525Q120 525 96 548T72 610ZM46 442L136 446L226 450H232V62H294V0H286Q271 3 171 3Q67 3 49 0H40V62H109V209Q109 358 108 362Q103 380 55 380H43V442H46Z"></path><path id="MJX-5-TEX-B-1D426" d="M40 442Q217 450 218 450H224V365Q226 367 235 378T254 397T278 416T314 435T362 448Q376 450 400 450H406Q503 450 534 393Q545 376 545 370Q545 368 555 379Q611 450 716 450Q774 450 809 434Q850 414 861 379T873 276V213V198V62H942V0H933Q915 3 809 3Q702 3 684 0H675V62H744V194V275Q744 348 735 373T690 399Q645 399 607 370T557 290Q555 281 554 171V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D413" xlink:href="#MJX-5-TEX-B-1D413"></use><use data-c="1D422" xlink:href="#MJX-5-TEX-B-1D422" transform="translate(800,0)"></use><use data-c="1D426" xlink:href="#MJX-5-TEX-B-1D426" transform="translate(1119,0)"></use></g></g></g></g></svg></mjx-container> — компілятор STG Тіма Олсона з синтаксисом Miranda.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.452ex;" xmlns="http://www.w3.org/2000/svg" width="6.321ex" height="2.025ex" role="img" focusable="false" viewBox="0 -695 2794 895" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-6-TEX-B-1D404" d="M723 286Q721 284 700 145T677 3V0H39V62H147V618H39V680H660V676Q662 670 675 552T691 428V424H629V428Q629 429 627 448T618 494T601 541Q574 593 527 605T382 618H374H304V384H336Q338 384 347 384T361 384T376 386T392 390T407 397T421 407T432 423Q442 444 443 482V501H505V205H443V224Q442 258 435 278T411 307T380 318T336 322H304V62H375H394Q429 62 449 62T497 66T541 76T577 95T609 126T632 170T651 232Q661 287 661 289H723V286Z"></path><path id="MJX-6-TEX-B-1D422" d="M72 610Q72 649 98 672T159 695Q193 693 217 670T241 610Q241 572 217 549T157 525Q120 525 96 548T72 610ZM46 442L136 446L226 450H232V62H294V0H286Q271 3 171 3Q67 3 49 0H40V62H109V209Q109 358 108 362Q103 380 55 380H43V442H46Z"></path><path id="MJX-6-TEX-B-1D423" d="M104 610Q104 649 130 672T191 695Q225 693 249 670T273 610Q273 572 249 549T189 525Q152 525 128 548T104 610ZM78 442L173 446L268 450H274V196Q274 -5 274 -37T269 -83Q256 -132 201 -166T71 -200Q10 -200 -30 -173T-71 -102Q-71 -70 -51 -51T-1 -31Q27 -31 48 -49T69 -100Q69 -121 53 -147H56Q66 -149 77 -149H80Q90 -149 100 -146T127 -125T149 -73Q151 -55 151 149V362Q150 364 148 366T145 370T142 373T138 375T133 377T124 378T113 379T97 380H75V442H78Z"></path><path id="MJX-6-TEX-B-1D42B" d="M405 293T374 293T324 312T305 361Q305 378 312 394Q315 397 315 399Q305 399 294 394T266 375T238 329T222 249Q221 241 221 149V62H308V0H298Q280 3 161 3Q47 3 38 0H29V62H98V210V303Q98 353 96 363T83 376Q69 380 42 380H29V442H32L118 446Q204 450 205 450H210V414L211 378Q247 449 315 449H321Q384 449 413 422T442 360Q442 332 424 313Z"></path><path id="MJX-6-TEX-B-1D428" d="M287 -5Q228 -5 182 10T109 48T63 102T39 161T32 219Q32 272 50 314T94 382T154 423T214 446T265 452H279Q319 452 326 451Q428 439 485 376T542 221Q542 156 514 108T442 33Q384 -5 287 -5ZM399 230V250Q399 280 398 298T391 338T372 372T338 392T282 401Q241 401 212 380Q190 363 183 334T175 230Q175 202 175 189T177 153T183 118T195 91T215 68T245 56T287 50Q348 50 374 84Q388 101 393 132T399 230Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D404" xlink:href="#MJX-6-TEX-B-1D404"></use><use data-c="1D422" xlink:href="#MJX-6-TEX-B-1D422" transform="translate(756,0)"></use><use data-c="1D423" xlink:href="#MJX-6-TEX-B-1D423" transform="translate(1075,0)"></use><use data-c="1D422" xlink:href="#MJX-6-TEX-B-1D422" transform="translate(1426,0)"></use><use data-c="1D42B" xlink:href="#MJX-6-TEX-B-1D42B" transform="translate(1745,0)"></use><use data-c="1D428" xlink:href="#MJX-6-TEX-B-1D428" transform="translate(2219,0)"></use></g></g></g></g></svg></mjx-container> — компілятор Ейджиро Сумії з синтаксисом MiniCaml.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.025ex;" xmlns="http://www.w3.org/2000/svg" width="6.864ex" height="1.597ex" role="img" focusable="false" viewBox="0 -695 3034 706" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-7-TEX-B-1D411" d="M394 0Q370 3 222 3Q75 3 51 0H39V62H147V624H39V686H234Q256 686 299 686T362 687Q479 687 554 669T681 593Q716 550 716 497Q716 390 568 338Q569 337 572 336T577 332Q605 317 623 300T650 258T662 218T668 172Q678 98 689 76Q707 40 748 40Q770 40 780 54T795 88T801 111Q805 117 827 117H831Q846 117 852 113T858 92Q857 78 852 63T834 30T797 1T739 -11Q630 -11 580 12T511 87Q506 104 506 168Q506 170 506 178T507 194Q507 289 438 313Q424 318 356 318H298V62H406V0H394ZM366 369Q459 370 490 381Q548 402 548 476V498V517Q548 578 513 600Q479 624 392 624H358H298V369H366Z"></path><path id="MJX-7-TEX-B-1D428" d="M287 -5Q228 -5 182 10T109 48T63 102T39 161T32 219Q32 272 50 314T94 382T154 423T214 446T265 452H279Q319 452 326 451Q428 439 485 376T542 221Q542 156 514 108T442 33Q384 -5 287 -5ZM399 230V250Q399 280 398 298T391 338T372 372T338 392T282 401Q241 401 212 380Q190 363 183 334T175 230Q175 202 175 189T177 153T183 118T195 91T215 68T245 56T287 50Q348 50 374 84Q388 101 393 132T399 230Z"></path><path id="MJX-7-TEX-B-1D41B" d="M32 686L123 690Q214 694 215 694H221V409Q289 450 378 450Q479 450 539 387T600 221Q600 122 535 58T358 -6H355Q272 -6 203 53L160 1L129 0H98V301Q98 362 98 435T99 525Q99 591 97 604T83 620Q69 624 42 624H29V686H32ZM227 105L232 99Q237 93 242 87T258 73T280 59T306 49T339 45Q380 45 411 66T451 131Q457 160 457 230Q457 264 456 284T448 329T430 367T396 389T343 398Q282 398 235 355L227 348V105Z"></path><path id="MJX-7-TEX-B-1D422" d="M72 610Q72 649 98 672T159 695Q193 693 217 670T241 610Q241 572 217 549T157 525Q120 525 96 548T72 610ZM46 442L136 446L226 450H232V62H294V0H286Q271 3 171 3Q67 3 49 0H40V62H109V209Q109 358 108 362Q103 380 55 380H43V442H46Z"></path><path id="MJX-7-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D411" xlink:href="#MJX-7-TEX-B-1D411"></use><use data-c="1D428" xlink:href="#MJX-7-TEX-B-1D428" transform="translate(862,0)"></use><use data-c="1D41B" xlink:href="#MJX-7-TEX-B-1D41B" transform="translate(1437,0)"></use><use data-c="1D422" xlink:href="#MJX-7-TEX-B-1D422" transform="translate(2076,0)"></use><use data-c="1D427" xlink:href="#MJX-7-TEX-B-1D427" transform="translate(2395,0)"></use></g></g></g></g></svg></mjx-container> — мова Робіна Мілнера для BLAS 3 на основі Standard ML.
</p><section><h1>Мови програмування</h1></section><p>Розділ присвячений таксономії мов програмування для доведення теорем — від
<a href="https://henk.groupoid.space">найпростіших</a> з квантором узагальнення до
<a href="https://anders.groupoid.space">гомотопічних систем</a> з двома рівностями.
Кінцева мета — створення прототипів верифікаторів для <a href="https://laurent.groupoid.space">функціонального аналізу</a>
і <a href="https://urs.groupoid.space">квантової супергеометрії</a>.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="6.048ex" height="1.584ex" role="img" focusable="false" viewBox="0 -694 2673 700" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-8-TEX-B-1D407" d="M400 0Q376 3 226 3Q75 3 51 0H39V62H147V624H39V686H51Q75 683 226 683Q376 683 400 686H412V624H304V388H595V624H487V686H499Q523 683 673 683Q824 683 848 686H860V624H752V62H860V0H848Q824 3 674 3Q523 3 499 0H487V62H595V326H304V62H412V0H400Z"></path><path id="MJX-8-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-8-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-8-TEX-B-1D424" d="M32 686L123 690Q214 694 215 694H221V255L377 382H346V444H355Q370 441 476 441Q544 441 556 444H562V382H476L347 277L515 62H587V0H579Q564 3 476 3Q370 3 352 0H343V62H358L373 63L260 206L237 189L216 172V62H285V0H277Q259 3 157 3Q46 3 37 0H29V62H98V332Q98 387 98 453T99 534Q99 593 97 605T83 620Q69 624 42 624H29V686H32Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D407" xlink:href="#MJX-8-TEX-B-1D407"></use><use data-c="1D41E" xlink:href="#MJX-8-TEX-B-1D41E" transform="translate(900,0)"></use><use data-c="1D427" xlink:href="#MJX-8-TEX-B-1D427" transform="translate(1427,0)"></use><use data-c="1D424" xlink:href="#MJX-8-TEX-B-1D424" transform="translate(2066,0)"></use></g></g></g></g></svg></mjx-container> — чиста система з всвесвітами.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="6.794ex" height="1.584ex" role="img" focusable="false" viewBox="0 -694 3003 700" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-9-TEX-B-1D405" d="M425 0L228 3Q63 3 51 0H39V62H147V618H39V680H644V676Q647 670 659 552T675 428V424H613Q613 433 605 477Q599 511 589 535T562 574T530 599T488 612T441 617T387 618H368H304V371H333Q389 373 411 390T437 468V488H499V192H437V212Q436 244 430 263T408 292T378 305T333 309H304V62H439V0H425Z"></path><path id="MJX-9-TEX-B-1D42B" d="M405 293T374 293T324 312T305 361Q305 378 312 394Q315 397 315 399Q305 399 294 394T266 375T238 329T222 249Q221 241 221 149V62H308V0H298Q280 3 161 3Q47 3 38 0H29V62H98V210V303Q98 353 96 363T83 376Q69 380 42 380H29V442H32L118 446Q204 450 205 450H210V414L211 378Q247 449 315 449H321Q384 449 413 422T442 360Q442 332 424 313Z"></path><path id="MJX-9-TEX-B-1D41A" d="M64 349Q64 399 107 426T255 453Q346 453 402 423T473 341Q478 327 478 310T479 196V77Q493 63 529 62Q549 62 553 57T558 31Q558 9 552 5T514 0H497H481Q375 0 367 56L356 46Q300 -6 210 -6Q130 -6 81 30T32 121Q32 188 111 226T332 272H350V292Q350 313 348 327T337 361T306 391T248 402T194 399H189Q204 376 204 354Q204 327 187 306T134 284Q97 284 81 305T64 349ZM164 121Q164 89 186 67T238 45Q274 45 307 63T346 108L350 117V226H347Q248 218 206 189T164 121Z"></path><path id="MJX-9-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-9-TEX-B-1D424" d="M32 686L123 690Q214 694 215 694H221V255L377 382H346V444H355Q370 441 476 441Q544 441 556 444H562V382H476L347 277L515 62H587V0H579Q564 3 476 3Q370 3 352 0H343V62H358L373 63L260 206L237 189L216 172V62H285V0H277Q259 3 157 3Q46 3 37 0H29V62H98V332Q98 387 98 453T99 534Q99 593 97 605T83 620Q69 624 42 624H29V686H32Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D405" xlink:href="#MJX-9-TEX-B-1D405"></use><use data-c="1D42B" xlink:href="#MJX-9-TEX-B-1D42B" transform="translate(724,0)"></use><use data-c="1D41A" xlink:href="#MJX-9-TEX-B-1D41A" transform="translate(1198,0)"></use><use data-c="1D427" xlink:href="#MJX-9-TEX-B-1D427" transform="translate(1757,0)"></use><use data-c="1D424" xlink:href="#MJX-9-TEX-B-1D424" transform="translate(2396,0)"></use></g></g></g></g></svg></mjx-container> — мінімальна індуктивна система.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.025ex;" xmlns="http://www.w3.org/2000/svg" width="10.518ex" height="1.602ex" role="img" focusable="false" viewBox="0 -697 4649 708" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-10-TEX-B-1D402" d="M64 343Q64 502 174 599T468 697Q502 697 533 691T586 674T623 655T647 639T657 632L694 663Q703 670 711 677T723 687T730 692T735 695T740 696T746 697Q759 697 762 692T766 668V627V489V449Q766 428 762 424T742 419H732H720Q699 419 697 436Q690 498 657 545Q611 618 532 632Q522 634 496 634Q356 634 286 553Q232 488 232 343T286 133Q355 52 497 52Q597 52 650 112T704 237Q704 248 709 251T729 254H735Q750 254 755 253T763 248T766 234Q766 136 680 63T469 -11Q285 -11 175 86T64 343Z"></path><path id="MJX-10-TEX-B-1D421" d="M40 686L131 690Q222 694 223 694H229V533L230 372L238 381Q248 394 264 407T317 435T398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V332Q106 387 106 453T107 534Q107 593 105 605T91 620Q77 624 50 624H37V686H40Z"></path><path id="MJX-10-TEX-B-1D42B" d="M405 293T374 293T324 312T305 361Q305 378 312 394Q315 397 315 399Q305 399 294 394T266 375T238 329T222 249Q221 241 221 149V62H308V0H298Q280 3 161 3Q47 3 38 0H29V62H98V210V303Q98 353 96 363T83 376Q69 380 42 380H29V442H32L118 446Q204 450 205 450H210V414L211 378Q247 449 315 449H321Q384 449 413 422T442 360Q442 332 424 313Z"></path><path id="MJX-10-TEX-B-1D422" d="M72 610Q72 649 98 672T159 695Q193 693 217 670T241 610Q241 572 217 549T157 525Q120 525 96 548T72 610ZM46 442L136 446L226 450H232V62H294V0H286Q271 3 171 3Q67 3 49 0H40V62H109V209Q109 358 108 362Q103 380 55 380H43V442H46Z"></path><path id="MJX-10-TEX-B-1D42C" d="M38 315Q38 339 45 360T70 404T127 440T223 453Q273 453 320 436L338 445L357 453H366Q380 453 383 447T386 403V387V355Q386 331 383 326T365 321H355H349Q333 321 329 324T324 341Q317 406 224 406H216Q123 406 123 353Q123 334 143 321T188 304T244 294T285 286Q305 281 325 273T373 237T412 172Q414 162 414 142Q414 -6 230 -6Q154 -6 117 22L68 -6H58Q44 -6 41 0T38 42V73Q38 85 38 101T37 122Q37 144 42 148T68 153H75Q87 153 91 151T97 147T103 132Q131 46 220 46H230Q257 46 265 47Q330 58 330 108Q330 127 316 142Q300 156 284 162Q271 168 212 178T122 202Q38 243 38 315Z"></path><path id="MJX-10-TEX-B-1D42D" d="M272 49Q320 49 320 136V145V177H382V143Q382 106 380 99Q374 62 349 36T285 -2L272 -5H247Q173 -5 134 27Q109 46 102 74T94 160Q94 171 94 199T95 245V382H21V433H25Q58 433 90 456Q121 479 140 523T162 621V635H224V444H363V382H224V239V207V149Q224 98 228 81T249 55Q261 49 272 49Z"></path><path id="MJX-10-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-10-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D402" xlink:href="#MJX-10-TEX-B-1D402"></use><use data-c="1D421" xlink:href="#MJX-10-TEX-B-1D421" transform="translate(831,0)"></use><use data-c="1D42B" xlink:href="#MJX-10-TEX-B-1D42B" transform="translate(1470,0)"></use><use data-c="1D422" xlink:href="#MJX-10-TEX-B-1D422" transform="translate(1944,0)"></use><use data-c="1D42C" xlink:href="#MJX-10-TEX-B-1D42C" transform="translate(2263,0)"></use><use data-c="1D42D" xlink:href="#MJX-10-TEX-B-1D42D" transform="translate(2717,0)"></use><use data-c="1D422" xlink:href="#MJX-10-TEX-B-1D422" transform="translate(3164,0)"></use><use data-c="1D427" xlink:href="#MJX-10-TEX-B-1D427" transform="translate(3483,0)"></use><use data-c="1D41E" xlink:href="#MJX-10-TEX-B-1D41E" transform="translate(4122,0)"></use></g></g></g></g></svg></mjx-container> — тактична система доведення теорем.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="4.043ex" height="1.566ex" role="img" focusable="false" viewBox="0 -686 1787 692" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-11-TEX-B-1D40F" d="M400 0Q376 3 226 3Q75 3 51 0H39V62H147V624H39V686H253Q435 686 470 685T536 678Q585 668 621 648T675 605T705 557T718 514T721 483T718 451T704 409T673 362T616 322T530 293Q500 288 399 287H304V62H412V0H400ZM553 475Q553 554 537 582T459 622Q451 623 373 624H298V343H372Q457 344 480 350Q527 362 540 390T553 475Z"></path><path id="MJX-11-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-11-TEX-B-1D42B" d="M405 293T374 293T324 312T305 361Q305 378 312 394Q315 397 315 399Q305 399 294 394T266 375T238 329T222 249Q221 241 221 149V62H308V0H298Q280 3 161 3Q47 3 38 0H29V62H98V210V303Q98 353 96 363T83 376Q69 380 42 380H29V442H32L118 446Q204 450 205 450H210V414L211 378Q247 449 315 449H321Q384 449 413 422T442 360Q442 332 424 313Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D40F" xlink:href="#MJX-11-TEX-B-1D40F"></use><use data-c="1D41E" xlink:href="#MJX-11-TEX-B-1D41E" transform="translate(786,0)"></use><use data-c="1D42B" xlink:href="#MJX-11-TEX-B-1D42B" transform="translate(1313,0)"></use></g></g></g></g></svg></mjx-container> — внутрішня мова локальних ДЗК.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="8.149ex" height="1.593ex" role="img" focusable="false" viewBox="0 -698 3602 704" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-12-TEX-B-1D400" d="M296 0Q278 3 164 3Q58 3 49 0H40V62H92Q144 62 144 64Q388 682 397 689Q403 698 434 698Q463 698 471 689Q475 686 538 530T663 218L724 64Q724 62 776 62H828V0H817Q796 3 658 3Q509 3 485 0H472V62H517Q561 62 561 63L517 175H262L240 120Q218 65 217 64Q217 62 261 62H306V0H296ZM390 237L492 238L440 365Q390 491 388 491Q287 239 287 237H390Z"></path><path id="MJX-12-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-12-TEX-B-1D41D" d="M351 686L442 690Q533 694 534 694H540V389Q540 327 540 253T539 163Q539 97 541 83T555 66Q569 62 596 62H609V31Q609 0 608 0Q588 0 510 -3T412 -6Q411 -6 411 16V38L401 31Q337 -6 265 -6Q159 -6 99 58T38 224Q38 265 51 303T92 375T165 429T272 449Q359 449 417 412V507V555Q417 597 415 607T402 620Q388 624 361 624H348V686H351ZM411 350Q362 399 291 399Q278 399 256 392T218 371Q195 351 189 320T182 238V221Q182 179 183 159T191 115T212 74Q241 46 288 46Q358 46 404 100L411 109V350Z"></path><path id="MJX-12-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-12-TEX-B-1D42B" d="M405 293T374 293T324 312T305 361Q305 378 312 394Q315 397 315 399Q305 399 294 394T266 375T238 329T222 249Q221 241 221 149V62H308V0H298Q280 3 161 3Q47 3 38 0H29V62H98V210V303Q98 353 96 363T83 376Q69 380 42 380H29V442H32L118 446Q204 450 205 450H210V414L211 378Q247 449 315 449H321Q384 449 413 422T442 360Q442 332 424 313Z"></path><path id="MJX-12-TEX-B-1D42C" d="M38 315Q38 339 45 360T70 404T127 440T223 453Q273 453 320 436L338 445L357 453H366Q380 453 383 447T386 403V387V355Q386 331 383 326T365 321H355H349Q333 321 329 324T324 341Q317 406 224 406H216Q123 406 123 353Q123 334 143 321T188 304T244 294T285 286Q305 281 325 273T373 237T412 172Q414 162 414 142Q414 -6 230 -6Q154 -6 117 22L68 -6H58Q44 -6 41 0T38 42V73Q38 85 38 101T37 122Q37 144 42 148T68 153H75Q87 153 91 151T97 147T103 132Q131 46 220 46H230Q257 46 265 47Q330 58 330 108Q330 127 316 142Q300 156 284 162Q271 168 212 178T122 202Q38 243 38 315Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D400" xlink:href="#MJX-12-TEX-B-1D400"></use><use data-c="1D427" xlink:href="#MJX-12-TEX-B-1D427" transform="translate(869,0)"></use><use data-c="1D41D" xlink:href="#MJX-12-TEX-B-1D41D" transform="translate(1508,0)"></use><use data-c="1D41E" xlink:href="#MJX-12-TEX-B-1D41E" transform="translate(2147,0)"></use><use data-c="1D42B" xlink:href="#MJX-12-TEX-B-1D42B" transform="translate(2674,0)"></use><use data-c="1D42C" xlink:href="#MJX-12-TEX-B-1D42C" transform="translate(3148,0)"></use></g></g></g></g></svg></mjx-container> — гомотопічна система з двома рівностями.
</p><p>Повний перелік теорій типів, представлений в роботі:
1) Теорія типів Генка Барендрегта для чистого залежного лямбда-числення;
2) Теорія типів Пера Мартіна-Льофа для фібріційного контексту та індуктивних типів;
3) Теорія типів Андерса Мьортберга для початкового завантаження CCHM/CHM/HTS;
4) Симпліціальна гомотопічна теорія типів Дана Кана;
5) Теорія типів Джека Морави для хроматичної гомотопічної теорії та K-теорії;
6) Теорія типів Урса Шрайбера для еквіваріантної супeргеометрії;
7) Теорія типів Фаб’єна Мореля для A¹-гомотопічної теорії;
8) Теорія типів Лорана Шварца для функціонального аналізу та теорії розподілів;
9) Теорія типів Ернста Цермело для ZFC з законом виключеного третього;
10) Теорія типів Пола Коена для системи кардиналів, що включає великі кардинали та форсинг.
</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="8.998ex" height="1.566ex" role="img" focusable="false" viewBox="0 -686 3977 692" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-13-TEX-B-1D40B" d="M643 285Q641 280 629 148T612 4V0H39V62H147V624H39V686H51Q75 683 228 683Q415 685 425 686H439V624H304V62H352H378Q492 62 539 138Q551 156 558 178T569 214T576 255T581 289H643V285Z"></path><path id="MJX-13-TEX-B-1D41A" d="M64 349Q64 399 107 426T255 453Q346 453 402 423T473 341Q478 327 478 310T479 196V77Q493 63 529 62Q549 62 553 57T558 31Q558 9 552 5T514 0H497H481Q375 0 367 56L356 46Q300 -6 210 -6Q130 -6 81 30T32 121Q32 188 111 226T332 272H350V292Q350 313 348 327T337 361T306 391T248 402T194 399H189Q204 376 204 354Q204 327 187 306T134 284Q97 284 81 305T64 349ZM164 121Q164 89 186 67T238 45Q274 45 307 63T346 108L350 117V226H347Q248 218 206 189T164 121Z"></path><path id="MJX-13-TEX-B-1D42E" d="M40 442L134 446Q228 450 229 450H235V273V165Q235 90 238 74T254 52Q268 46 304 46H319Q352 46 380 67T419 121L420 123Q424 135 425 199Q425 201 425 207Q425 233 425 249V316Q425 354 423 363T410 376Q396 380 369 380H356V442L554 450V267Q554 84 556 79Q561 62 610 62H623V31Q623 0 622 0Q603 0 527 -3T432 -6Q431 -6 431 25V56L420 45Q373 6 332 -1Q313 -6 281 -6Q208 -6 165 14T109 87L107 98L106 230Q106 358 104 366Q96 380 50 380H37V442H40Z"></path><path id="MJX-13-TEX-B-1D42B" d="M405 293T374 293T324 312T305 361Q305 378 312 394Q315 397 315 399Q305 399 294 394T266 375T238 329T222 249Q221 241 221 149V62H308V0H298Q280 3 161 3Q47 3 38 0H29V62H98V210V303Q98 353 96 363T83 376Q69 380 42 380H29V442H32L118 446Q204 450 205 450H210V414L211 378Q247 449 315 449H321Q384 449 413 422T442 360Q442 332 424 313Z"></path><path id="MJX-13-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-13-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-13-TEX-B-1D42D" d="M272 49Q320 49 320 136V145V177H382V143Q382 106 380 99Q374 62 349 36T285 -2L272 -5H247Q173 -5 134 27Q109 46 102 74T94 160Q94 171 94 199T95 245V382H21V433H25Q58 433 90 456Q121 479 140 523T162 621V635H224V444H363V382H224V239V207V149Q224 98 228 81T249 55Q261 49 272 49Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D40B" xlink:href="#MJX-13-TEX-B-1D40B"></use><use data-c="1D41A" xlink:href="#MJX-13-TEX-B-1D41A" transform="translate(692,0)"></use><use data-c="1D42E" xlink:href="#MJX-13-TEX-B-1D42E" transform="translate(1251,0)"></use><use data-c="1D42B" xlink:href="#MJX-13-TEX-B-1D42B" transform="translate(1890,0)"></use><use data-c="1D41E" xlink:href="#MJX-13-TEX-B-1D41E" transform="translate(2364,0)"></use><use data-c="1D427" xlink:href="#MJX-13-TEX-B-1D427" transform="translate(2891,0)"></use><use data-c="1D42D" xlink:href="#MJX-13-TEX-B-1D42D" transform="translate(3530,0)"></use></g></g></g></g></svg></mjx-container> — система типів функціонального аналізу.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="4.706ex" height="1.566ex" role="img" focusable="false" viewBox="0 -686 2080 692" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-14-TEX-B-1D403" d="M39 624V686H270H310H408Q500 686 545 680T638 649Q768 584 805 438Q817 388 817 338Q817 171 702 75Q628 17 515 2Q504 1 270 0H39V62H147V624H39ZM655 337Q655 370 655 390T650 442T639 494T616 540T580 580T526 607T451 623Q443 624 368 624H298V62H377H387H407Q445 62 472 65T540 83T606 129Q629 156 640 195T653 262T655 337Z"></path><path id="MJX-14-TEX-B-1D41A" d="M64 349Q64 399 107 426T255 453Q346 453 402 423T473 341Q478 327 478 310T479 196V77Q493 63 529 62Q549 62 553 57T558 31Q558 9 552 5T514 0H497H481Q375 0 367 56L356 46Q300 -6 210 -6Q130 -6 81 30T32 121Q32 188 111 226T332 272H350V292Q350 313 348 327T337 361T306 391T248 402T194 399H189Q204 376 204 354Q204 327 187 306T134 284Q97 284 81 305T64 349ZM164 121Q164 89 186 67T238 45Q274 45 307 63T346 108L350 117V226H347Q248 218 206 189T164 121Z"></path><path id="MJX-14-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D403" xlink:href="#MJX-14-TEX-B-1D403"></use><use data-c="1D41A" xlink:href="#MJX-14-TEX-B-1D41A" transform="translate(882,0)"></use><use data-c="1D427" xlink:href="#MJX-14-TEX-B-1D427" transform="translate(1441,0)"></use></g></g></g></g></svg></mjx-container> — сімпліціальна теорія інфініті-категорій.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.025ex;" xmlns="http://www.w3.org/2000/svg" width="5.138ex" height="1.595ex" role="img" focusable="false" viewBox="0 -694 2271 705" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-15-TEX-B-1D409" d="M174 114Q174 96 169 82T159 63T144 47L155 45Q183 40 203 40Q271 40 290 104Q294 118 294 150T295 380V624H154V686H169Q196 683 365 683Q499 683 517 686H527V624H446V379Q446 183 446 153T441 108Q413 32 315 2Q266 -11 208 -11Q160 -11 118 -2T42 37T8 114V122Q8 150 30 174T91 198T152 174T174 122V114Z"></path><path id="MJX-15-TEX-B-1D41A" d="M64 349Q64 399 107 426T255 453Q346 453 402 423T473 341Q478 327 478 310T479 196V77Q493 63 529 62Q549 62 553 57T558 31Q558 9 552 5T514 0H497H481Q375 0 367 56L356 46Q300 -6 210 -6Q130 -6 81 30T32 121Q32 188 111 226T332 272H350V292Q350 313 348 327T337 361T306 391T248 402T194 399H189Q204 376 204 354Q204 327 187 306T134 284Q97 284 81 305T64 349ZM164 121Q164 89 186 67T238 45Q274 45 307 63T346 108L350 117V226H347Q248 218 206 189T164 121Z"></path><path id="MJX-15-TEX-B-1D41C" d="M447 131H458Q478 131 478 117Q478 112 471 95T439 51T377 9Q330 -6 286 -6Q196 -6 135 35Q39 96 39 222Q39 324 101 384Q169 453 286 453Q359 453 411 431T464 353Q464 319 445 302T395 284Q360 284 343 305T325 353Q325 380 338 396H333Q317 398 295 398H292Q280 398 271 397T245 390T218 373T197 338T183 283Q182 275 182 231Q182 199 184 180T193 132T220 85T270 57Q289 50 317 50H326Q385 50 414 115Q419 127 423 129T447 131Z"></path><path id="MJX-15-TEX-B-1D424" d="M32 686L123 690Q214 694 215 694H221V255L377 382H346V444H355Q370 441 476 441Q544 441 556 444H562V382H476L347 277L515 62H587V0H579Q564 3 476 3Q370 3 352 0H343V62H358L373 63L260 206L237 189L216 172V62H285V0H277Q259 3 157 3Q46 3 37 0H29V62H98V332Q98 387 98 453T99 534Q99 593 97 605T83 620Q69 624 42 624H29V686H32Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D409" xlink:href="#MJX-15-TEX-B-1D409"></use><use data-c="1D41A" xlink:href="#MJX-15-TEX-B-1D41A" transform="translate(594,0)"></use><use data-c="1D41C" xlink:href="#MJX-15-TEX-B-1D41C" transform="translate(1153,0)"></use><use data-c="1D424" xlink:href="#MJX-15-TEX-B-1D424" transform="translate(1664,0)"></use></g></g></g></g></svg></mjx-container> — синтетична К-теорія.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.014ex;" xmlns="http://www.w3.org/2000/svg" width="7.708ex" height="1.586ex" role="img" focusable="false" viewBox="0 -695 3407 701" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-16-TEX-B-1D405" d="M425 0L228 3Q63 3 51 0H39V62H147V618H39V680H644V676Q647 670 659 552T675 428V424H613Q613 433 605 477Q599 511 589 535T562 574T530 599T488 612T441 617T387 618H368H304V371H333Q389 373 411 390T437 468V488H499V192H437V212Q436 244 430 263T408 292T378 305T333 309H304V62H439V0H425Z"></path><path id="MJX-16-TEX-B-1D41A" d="M64 349Q64 399 107 426T255 453Q346 453 402 423T473 341Q478 327 478 310T479 196V77Q493 63 529 62Q549 62 553 57T558 31Q558 9 552 5T514 0H497H481Q375 0 367 56L356 46Q300 -6 210 -6Q130 -6 81 30T32 121Q32 188 111 226T332 272H350V292Q350 313 348 327T337 361T306 391T248 402T194 399H189Q204 376 204 354Q204 327 187 306T134 284Q97 284 81 305T64 349ZM164 121Q164 89 186 67T238 45Q274 45 307 63T346 108L350 117V226H347Q248 218 206 189T164 121Z"></path><path id="MJX-16-TEX-B-1D41B" d="M32 686L123 690Q214 694 215 694H221V409Q289 450 378 450Q479 450 539 387T600 221Q600 122 535 58T358 -6H355Q272 -6 203 53L160 1L129 0H98V301Q98 362 98 435T99 525Q99 591 97 604T83 620Q69 624 42 624H29V686H32ZM227 105L232 99Q237 93 242 87T258 73T280 59T306 49T339 45Q380 45 411 66T451 131Q457 160 457 230Q457 264 456 284T448 329T430 367T396 389T343 398Q282 398 235 355L227 348V105Z"></path><path id="MJX-16-TEX-B-1D422" d="M72 610Q72 649 98 672T159 695Q193 693 217 670T241 610Q241 572 217 549T157 525Q120 525 96 548T72 610ZM46 442L136 446L226 450H232V62H294V0H286Q271 3 171 3Q67 3 49 0H40V62H109V209Q109 358 108 362Q103 380 55 380H43V442H46Z"></path><path id="MJX-16-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-16-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D405" xlink:href="#MJX-16-TEX-B-1D405"></use><use data-c="1D41A" xlink:href="#MJX-16-TEX-B-1D41A" transform="translate(724,0)"></use><use data-c="1D41B" xlink:href="#MJX-16-TEX-B-1D41B" transform="translate(1283,0)"></use><use data-c="1D422" xlink:href="#MJX-16-TEX-B-1D422" transform="translate(1922,0)"></use><use data-c="1D41E" xlink:href="#MJX-16-TEX-B-1D41E" transform="translate(2241,0)"></use><use data-c="1D427" xlink:href="#MJX-16-TEX-B-1D427" transform="translate(2768,0)"></use></g></g></g></g></svg></mjx-container> — <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: 0;" xmlns="http://www.w3.org/2000/svg" width="2.621ex" height="1.887ex" role="img" focusable="false" viewBox="0 -833.9 1158.6 833.9" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-17-TEX-D-1D538" d="M130 -1H63Q34 -1 26 2T17 17Q17 24 22 29T35 35Q49 35 64 44T88 66Q101 93 210 383Q331 693 335 697T346 701T357 697Q358 696 493 399Q621 104 633 83Q656 35 686 35Q693 35 698 30T703 17Q703 5 693 2T643 -1H541Q388 -1 386 1Q378 6 378 16Q378 24 383 29T397 35Q412 35 434 45T456 65Q456 93 428 170L419 197H197L195 179Q184 134 184 97Q184 82 186 71T190 55T198 45T205 39T214 36L219 35Q241 31 241 17Q241 5 233 2T196 -1H130ZM493 68Q493 51 481 35H619Q604 56 515 256Q486 321 468 361L348 637Q347 637 330 592T313 543Q313 538 358 436T448 219T493 68ZM404 235Q404 239 355 355T295 488L275 430Q241 348 208 232H306Q404 232 404 235ZM155 48Q151 55 148 88V117L135 86Q118 47 117 46L110 37L135 35H159Q157 41 155 48Z"></path><path id="MJX-17-TEX-N-31" d="M213 578L200 573Q186 568 160 563T102 556H83V602H102Q149 604 189 617T245 641T273 663Q275 666 285 666Q294 666 302 660V361L303 61Q310 54 315 52T339 48T401 46H427V0H416Q395 3 257 3Q121 3 100 0H88V46H114Q136 46 152 46T177 47T193 50T201 52T207 57T213 61V578Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="msup"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D538" xlink:href="#MJX-17-TEX-D-1D538"></use></g></g><g data-mml-node="mn" transform="translate(755,363) scale(0.707)"><use data-c="31" xlink:href="#MJX-17-TEX-N-31"></use></g></g></g></g></svg></mjx-container>-теорія гомотопій.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.025ex;" xmlns="http://www.w3.org/2000/svg" width="4.102ex" height="1.577ex" role="img" focusable="false" viewBox="0 -686 1813 697" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-18-TEX-B-1D414" d="M570 686Q588 683 703 683T836 686H845V624H737V420Q737 390 737 345T738 284Q738 205 729 164T689 83Q614 -11 465 -11Q321 -11 240 51T148 207Q147 214 147 421V624H39V686H51Q75 683 226 683Q376 683 400 686H412V624H304V405V370V268Q304 181 311 146T346 87Q387 52 466 52Q642 52 667 195Q668 204 669 415V624H561V686H570Z"></path><path id="MJX-18-TEX-B-1D42B" d="M405 293T374 293T324 312T305 361Q305 378 312 394Q315 397 315 399Q305 399 294 394T266 375T238 329T222 249Q221 241 221 149V62H308V0H298Q280 3 161 3Q47 3 38 0H29V62H98V210V303Q98 353 96 363T83 376Q69 380 42 380H29V442H32L118 446Q204 450 205 450H210V414L211 378Q247 449 315 449H321Q384 449 413 422T442 360Q442 332 424 313Z"></path><path id="MJX-18-TEX-B-1D42C" d="M38 315Q38 339 45 360T70 404T127 440T223 453Q273 453 320 436L338 445L357 453H366Q380 453 383 447T386 403V387V355Q386 331 383 326T365 321H355H349Q333 321 329 324T324 341Q317 406 224 406H216Q123 406 123 353Q123 334 143 321T188 304T244 294T285 286Q305 281 325 273T373 237T412 172Q414 162 414 142Q414 -6 230 -6Q154 -6 117 22L68 -6H58Q44 -6 41 0T38 42V73Q38 85 38 101T37 122Q37 144 42 148T68 153H75Q87 153 91 151T97 147T103 132Q131 46 220 46H230Q257 46 265 47Q330 58 330 108Q330 127 316 142Q300 156 284 162Q271 168 212 178T122 202Q38 243 38 315Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D414" xlink:href="#MJX-18-TEX-B-1D414"></use><use data-c="1D42B" xlink:href="#MJX-18-TEX-B-1D42B" transform="translate(885,0)"></use><use data-c="1D42C" xlink:href="#MJX-18-TEX-B-1D42C" transform="translate(1359,0)"></use></g></g></g></g></svg></mjx-container> — еквіваріантна система типів супергеометрії.
</p><section><h1>Формалізація математик</h1></section><p>Розділ присвячений механічній верифікації
математичних теорем, від класичного аналізу до сучасних теорій множин і гомотопій.
Система синтезує синтетичну гомотопію, стабільні гомотопічні спектри, когезивну геометрію,
дійсний аналіз і теорію множин у єдиному формалізмі.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.452ex;" xmlns="http://www.w3.org/2000/svg" width="9.548ex" height="2.032ex" role="img" focusable="false" viewBox="0 -698 4220 898" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-19-TEX-B-1D400" d="M296 0Q278 3 164 3Q58 3 49 0H40V62H92Q144 62 144 64Q388 682 397 689Q403 698 434 698Q463 698 471 689Q475 686 538 530T663 218L724 64Q724 62 776 62H828V0H817Q796 3 658 3Q509 3 485 0H472V62H517Q561 62 561 63L517 175H262L240 120Q218 65 217 64Q217 62 261 62H306V0H296ZM390 237L492 238L440 365Q390 491 388 491Q287 239 287 237H390Z"></path><path id="MJX-19-TEX-B-1D427" d="M40 442Q217 450 218 450H224V407L225 365Q233 378 245 391T289 422T362 448Q374 450 398 450Q428 450 448 447T491 434T529 402T551 346Q553 335 554 198V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-19-TEX-B-1D41A" d="M64 349Q64 399 107 426T255 453Q346 453 402 423T473 341Q478 327 478 310T479 196V77Q493 63 529 62Q549 62 553 57T558 31Q558 9 552 5T514 0H497H481Q375 0 367 56L356 46Q300 -6 210 -6Q130 -6 81 30T32 121Q32 188 111 226T332 272H350V292Q350 313 348 327T337 361T306 391T248 402T194 399H189Q204 376 204 354Q204 327 187 306T134 284Q97 284 81 305T64 349ZM164 121Q164 89 186 67T238 45Q274 45 307 63T346 108L350 117V226H347Q248 218 206 189T164 121Z"></path><path id="MJX-19-TEX-B-1D425" d="M43 686L134 690Q225 694 226 694H232V62H301V0H292Q274 3 170 3Q67 3 49 0H40V62H109V332Q109 387 109 453T110 534Q110 593 108 605T94 620Q80 624 53 624H40V686H43Z"></path><path id="MJX-19-TEX-B-1D432" d="M84 -102Q84 -110 87 -119T102 -138T133 -149Q148 -148 162 -143T186 -131T206 -114T222 -95T234 -76T243 -59T249 -45T252 -37L269 0L96 382H26V444H34Q49 441 146 441Q252 441 270 444H279V382H255Q232 382 232 380L337 151L442 382H394V444H401Q413 441 495 441Q568 441 574 444H580V382H510L406 152Q298 -84 297 -87Q269 -139 225 -169T131 -200Q85 -200 54 -172T23 -100Q23 -64 44 -50T87 -35Q111 -35 130 -50T152 -92V-100H84V-102Z"></path><path id="MJX-19-TEX-B-1D42C" d="M38 315Q38 339 45 360T70 404T127 440T223 453Q273 453 320 436L338 445L357 453H366Q380 453 383 447T386 403V387V355Q386 331 383 326T365 321H355H349Q333 321 329 324T324 341Q317 406 224 406H216Q123 406 123 353Q123 334 143 321T188 304T244 294T285 286Q305 281 325 273T373 237T412 172Q414 162 414 142Q414 -6 230 -6Q154 -6 117 22L68 -6H58Q44 -6 41 0T38 42V73Q38 85 38 101T37 122Q37 144 42 148T68 153H75Q87 153 91 151T97 147T103 132Q131 46 220 46H230Q257 46 265 47Q330 58 330 108Q330 127 316 142Q300 156 284 162Q271 168 212 178T122 202Q38 243 38 315Z"></path><path id="MJX-19-TEX-B-1D422" d="M72 610Q72 649 98 672T159 695Q193 693 217 670T241 610Q241 572 217 549T157 525Q120 525 96 548T72 610ZM46 442L136 446L226 450H232V62H294V0H286Q271 3 171 3Q67 3 49 0H40V62H109V209Q109 358 108 362Q103 380 55 380H43V442H46Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D400" xlink:href="#MJX-19-TEX-B-1D400"></use><use data-c="1D427" xlink:href="#MJX-19-TEX-B-1D427" transform="translate(869,0)"></use><use data-c="1D41A" xlink:href="#MJX-19-TEX-B-1D41A" transform="translate(1508,0)"></use><use data-c="1D425" xlink:href="#MJX-19-TEX-B-1D425" transform="translate(2067,0)"></use><use data-c="1D432" xlink:href="#MJX-19-TEX-B-1D432" transform="translate(2386,0)"></use><use data-c="1D42C" xlink:href="#MJX-19-TEX-B-1D42C" transform="translate(2993,0)"></use><use data-c="1D422" xlink:href="#MJX-19-TEX-B-1D422" transform="translate(3447,0)"></use><use data-c="1D42C" xlink:href="#MJX-19-TEX-B-1D42C" transform="translate(3766,0)"></use></g></g></g></g></svg></mjx-container> — теорія розподілів Лорана Шварца.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.455ex;" xmlns="http://www.w3.org/2000/svg" width="8.964ex" height="2.034ex" role="img" focusable="false" viewBox="0 -698 3962 899" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-20-TEX-B-1D400" d="M296 0Q278 3 164 3Q58 3 49 0H40V62H92Q144 62 144 64Q388 682 397 689Q403 698 434 698Q463 698 471 689Q475 686 538 530T663 218L724 64Q724 62 776 62H828V0H817Q796 3 658 3Q509 3 485 0H472V62H517Q561 62 561 63L517 175H262L240 120Q218 65 217 64Q217 62 261 62H306V0H296ZM390 237L492 238L440 365Q390 491 388 491Q287 239 287 237H390Z"></path><path id="MJX-20-TEX-B-1D425" d="M43 686L134 690Q225 694 226 694H232V62H301V0H292Q274 3 170 3Q67 3 49 0H40V62H109V332Q109 387 109 453T110 534Q110 593 108 605T94 620Q80 624 53 624H40V686H43Z"></path><path id="MJX-20-TEX-B-1D420" d="M50 300Q50 368 105 409T255 450Q328 450 376 426L388 420Q435 455 489 455Q517 455 533 441T554 414T558 389Q558 367 544 353T508 339Q484 339 471 354T458 387Q458 397 462 400Q464 401 461 400Q459 400 454 399Q429 392 427 390Q454 353 459 328Q461 315 461 300Q461 240 419 202Q364 149 248 149Q185 149 136 172Q129 158 129 148Q129 105 170 93Q176 91 263 91Q273 91 298 91T334 91T366 89T400 85T432 77T466 64Q544 22 544 -69Q544 -114 506 -145Q438 -201 287 -201Q149 -201 90 -161T30 -70Q30 -58 33 -47T42 -27T54 -13T69 -1T82 6T94 12T101 15Q66 57 66 106Q66 151 90 187L97 197L89 204Q50 243 50 300ZM485 403H492Q491 404 488 404L485 403V403ZM255 200Q279 200 295 206T319 219T331 242T335 268T336 300Q336 337 333 352T317 380Q298 399 255 399Q228 399 211 392T187 371T178 345T176 312V300V289Q176 235 194 219Q215 200 255 200ZM287 -150Q357 -150 400 -128T443 -71Q443 -65 442 -61T436 -50T420 -37T389 -27T339 -21L308 -20Q276 -20 253 -20Q190 -20 180 -20T156 -26Q130 -38 130 -69Q130 -105 173 -127T287 -150Z"></path><path id="MJX-20-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-20-TEX-B-1D41B" d="M32 686L123 690Q214 694 215 694H221V409Q289 450 378 450Q479 450 539 387T600 221Q600 122 535 58T358 -6H355Q272 -6 203 53L160 1L129 0H98V301Q98 362 98 435T99 525Q99 591 97 604T83 620Q69 624 42 624H29V686H32ZM227 105L232 99Q237 93 242 87T258 73T280 59T306 49T339 45Q380 45 411 66T451 131Q457 160 457 230Q457 264 456 284T448 329T430 367T396 389T343 398Q282 398 235 355L227 348V105Z"></path><path id="MJX-20-TEX-B-1D42B" d="M405 293T374 293T324 312T305 361Q305 378 312 394Q315 397 315 399Q305 399 294 394T266 375T238 329T222 249Q221 241 221 149V62H308V0H298Q280 3 161 3Q47 3 38 0H29V62H98V210V303Q98 353 96 363T83 376Q69 380 42 380H29V442H32L118 446Q204 450 205 450H210V414L211 378Q247 449 315 449H321Q384 449 413 422T442 360Q442 332 424 313Z"></path><path id="MJX-20-TEX-B-1D41A" d="M64 349Q64 399 107 426T255 453Q346 453 402 423T473 341Q478 327 478 310T479 196V77Q493 63 529 62Q549 62 553 57T558 31Q558 9 552 5T514 0H497H481Q375 0 367 56L356 46Q300 -6 210 -6Q130 -6 81 30T32 121Q32 188 111 226T332 272H350V292Q350 313 348 327T337 361T306 391T248 402T194 399H189Q204 376 204 354Q204 327 187 306T134 284Q97 284 81 305T64 349ZM164 121Q164 89 186 67T238 45Q274 45 307 63T346 108L350 117V226H347Q248 218 206 189T164 121Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D400" xlink:href="#MJX-20-TEX-B-1D400"></use><use data-c="1D425" xlink:href="#MJX-20-TEX-B-1D425" transform="translate(869,0)"></use><use data-c="1D420" xlink:href="#MJX-20-TEX-B-1D420" transform="translate(1188,0)"></use><use data-c="1D41E" xlink:href="#MJX-20-TEX-B-1D41E" transform="translate(1763,0)"></use><use data-c="1D41B" xlink:href="#MJX-20-TEX-B-1D41B" transform="translate(2290,0)"></use><use data-c="1D42B" xlink:href="#MJX-20-TEX-B-1D42B" transform="translate(2929,0)"></use><use data-c="1D41A" xlink:href="#MJX-20-TEX-B-1D41A" transform="translate(3403,0)"></use></g></g></g></g></svg></mjx-container> — гомологічна алгебра.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.452ex;" xmlns="http://www.w3.org/2000/svg" width="11.937ex" height="2.005ex" role="img" focusable="false" viewBox="0 -686 5276 886" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-21-TEX-B-1D407" d="M400 0Q376 3 226 3Q75 3 51 0H39V62H147V624H39V686H51Q75 683 226 683Q376 683 400 686H412V624H304V388H595V624H487V686H499Q523 683 673 683Q824 683 848 686H860V624H752V62H860V0H848Q824 3 674 3Q523 3 499 0H487V62H595V326H304V62H412V0H400Z"></path><path id="MJX-21-TEX-B-1D428" d="M287 -5Q228 -5 182 10T109 48T63 102T39 161T32 219Q32 272 50 314T94 382T154 423T214 446T265 452H279Q319 452 326 451Q428 439 485 376T542 221Q542 156 514 108T442 33Q384 -5 287 -5ZM399 230V250Q399 280 398 298T391 338T372 372T338 392T282 401Q241 401 212 380Q190 363 183 334T175 230Q175 202 175 189T177 153T183 118T195 91T215 68T245 56T287 50Q348 50 374 84Q388 101 393 132T399 230Z"></path><path id="MJX-21-TEX-B-1D426" d="M40 442Q217 450 218 450H224V365Q226 367 235 378T254 397T278 416T314 435T362 448Q376 450 400 450H406Q503 450 534 393Q545 376 545 370Q545 368 555 379Q611 450 716 450Q774 450 809 434Q850 414 861 379T873 276V213V198V62H942V0H933Q915 3 809 3Q702 3 684 0H675V62H744V194V275Q744 348 735 373T690 399Q645 399 607 370T557 290Q555 281 554 171V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-21-TEX-B-1D42D" d="M272 49Q320 49 320 136V145V177H382V143Q382 106 380 99Q374 62 349 36T285 -2L272 -5H247Q173 -5 134 27Q109 46 102 74T94 160Q94 171 94 199T95 245V382H21V433H25Q58 433 90 456Q121 479 140 523T162 621V635H224V444H363V382H224V239V207V149Q224 98 228 81T249 55Q261 49 272 49Z"></path><path id="MJX-21-TEX-B-1D429" d="M32 442L123 446Q214 450 215 450H221V409Q222 409 229 413T251 423T284 436T328 446T382 450Q480 450 540 388T600 223Q600 128 539 61T361 -6H354Q292 -6 236 28L227 34V-132H296V-194H287Q269 -191 163 -191Q56 -191 38 -194H29V-132H98V113V284Q98 330 97 348T93 370T83 376Q69 380 42 380H29V442H32ZM457 224Q457 303 427 349T350 395Q282 395 235 352L227 345V104L233 97Q274 45 337 45Q383 45 420 86T457 224Z"></path><path id="MJX-21-TEX-B-1D432" d="M84 -102Q84 -110 87 -119T102 -138T133 -149Q148 -148 162 -143T186 -131T206 -114T222 -95T234 -76T243 -59T249 -45T252 -37L269 0L96 382H26V444H34Q49 441 146 441Q252 441 270 444H279V382H255Q232 382 232 380L337 151L442 382H394V444H401Q413 441 495 441Q568 441 574 444H580V382H510L406 152Q298 -84 297 -87Q269 -139 225 -169T131 -200Q85 -200 54 -172T23 -100Q23 -64 44 -50T87 -35Q111 -35 130 -50T152 -92V-100H84V-102Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D407" xlink:href="#MJX-21-TEX-B-1D407"></use><use data-c="1D428" xlink:href="#MJX-21-TEX-B-1D428" transform="translate(900,0)"></use><use data-c="1D426" xlink:href="#MJX-21-TEX-B-1D426" transform="translate(1475,0)"></use><use data-c="1D428" xlink:href="#MJX-21-TEX-B-1D428" transform="translate(2433,0)"></use><use data-c="1D42D" xlink:href="#MJX-21-TEX-B-1D42D" transform="translate(3008,0)"></use><use data-c="1D428" xlink:href="#MJX-21-TEX-B-1D428" transform="translate(3455,0)"></use><use data-c="1D429" xlink:href="#MJX-21-TEX-B-1D429" transform="translate(4030,0)"></use><use data-c="1D432" xlink:href="#MJX-21-TEX-B-1D432" transform="translate(4669,0)"></use></g></g></g></g></svg></mjx-container> — теорія гомотопій.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.452ex;" xmlns="http://www.w3.org/2000/svg" width="11.355ex" height="2.029ex" role="img" focusable="false" viewBox="0 -697 5019 897" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-22-TEX-B-1D406" d="M465 -10Q281 -10 173 88T64 343Q64 413 85 471T143 568T217 631T298 670Q371 697 449 697Q452 697 459 697T470 696Q502 696 531 690T582 675T618 658T644 641T656 632L732 695Q734 697 745 697Q758 697 761 692T765 668V627V489V449Q765 428 761 424T741 419H731H724Q705 419 702 422T695 444Q683 520 631 577T495 635Q364 635 295 563Q261 528 247 477T232 343Q232 296 236 260T256 185T296 120T366 76T472 52Q481 51 498 51Q544 51 573 67T607 108Q608 111 608 164V214H464V276H479Q506 273 680 273Q816 273 834 276H845V214H765V113V51Q765 16 763 8T750 0Q742 2 709 16T658 40L648 46Q592 -10 465 -10Z"></path><path id="MJX-22-TEX-B-1D41E" d="M32 225Q32 332 102 392T272 452H283Q382 452 436 401Q494 343 494 243Q494 226 486 222T440 217Q431 217 394 217T327 218H175V209Q175 177 179 154T196 107T236 69T306 50Q312 49 323 49Q376 49 410 85Q421 99 427 111T434 127T442 133T463 135H468Q494 135 494 117Q494 110 489 97T468 66T431 32T373 5T292 -6Q181 -6 107 55T32 225ZM383 276Q377 346 348 374T280 402Q253 402 230 390T195 357Q179 331 176 279V266H383V276Z"></path><path id="MJX-22-TEX-B-1D428" d="M287 -5Q228 -5 182 10T109 48T63 102T39 161T32 219Q32 272 50 314T94 382T154 423T214 446T265 452H279Q319 452 326 451Q428 439 485 376T542 221Q542 156 514 108T442 33Q384 -5 287 -5ZM399 230V250Q399 280 398 298T391 338T372 372T338 392T282 401Q241 401 212 380Q190 363 183 334T175 230Q175 202 175 189T177 153T183 118T195 91T215 68T245 56T287 50Q348 50 374 84Q388 101 393 132T399 230Z"></path><path id="MJX-22-TEX-B-1D426" d="M40 442Q217 450 218 450H224V365Q226 367 235 378T254 397T278 416T314 435T362 448Q376 450 400 450H406Q503 450 534 393Q545 376 545 370Q545 368 555 379Q611 450 716 450Q774 450 809 434Q850 414 861 379T873 276V213V198V62H942V0H933Q915 3 809 3Q702 3 684 0H675V62H744V194V275Q744 348 735 373T690 399Q645 399 607 370T557 290Q555 281 554 171V62H623V0H614Q596 3 489 3Q374 3 365 0H356V62H425V194V275Q425 348 416 373T371 399Q326 399 288 370T238 290Q236 281 235 171V62H304V0H295Q277 3 171 3Q64 3 46 0H37V62H106V210V303Q106 353 104 363T91 376Q77 380 50 380H37V442H40Z"></path><path id="MJX-22-TEX-B-1D42D" d="M272 49Q320 49 320 136V145V177H382V143Q382 106 380 99Q374 62 349 36T285 -2L272 -5H247Q173 -5 134 27Q109 46 102 74T94 160Q94 171 94 199T95 245V382H21V433H25Q58 433 90 456Q121 479 140 523T162 621V635H224V444H363V382H224V239V207V149Q224 98 228 81T249 55Q261 49 272 49Z"></path><path id="MJX-22-TEX-B-1D42B" d="M405 293T374 293T324 312T305 361Q305 378 312 394Q315 397 315 399Q305 399 294 394T266 375T238 329T222 249Q221 241 221 149V62H308V0H298Q280 3 161 3Q47 3 38 0H29V62H98V210V303Q98 353 96 363T83 376Q69 380 42 380H29V442H32L118 446Q204 450 205 450H210V414L211 378Q247 449 315 449H321Q384 449 413 422T442 360Q442 332 424 313Z"></path><path id="MJX-22-TEX-B-1D432" d="M84 -102Q84 -110 87 -119T102 -138T133 -149Q148 -148 162 -143T186 -131T206 -114T222 -95T234 -76T243 -59T249 -45T252 -37L269 0L96 382H26V444H34Q49 441 146 441Q252 441 270 444H279V382H255Q232 382 232 380L337 151L442 382H394V444H401Q413 441 495 441Q568 441 574 444H580V382H510L406 152Q298 -84 297 -87Q269 -139 225 -169T131 -200Q85 -200 54 -172T23 -100Q23 -64 44 -50T87 -35Q111 -35 130 -50T152 -92V-100H84V-102Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D406" xlink:href="#MJX-22-TEX-B-1D406"></use><use data-c="1D41E" xlink:href="#MJX-22-TEX-B-1D41E" transform="translate(904,0)"></use><use data-c="1D428" xlink:href="#MJX-22-TEX-B-1D428" transform="translate(1431,0)"></use><use data-c="1D426" xlink:href="#MJX-22-TEX-B-1D426" transform="translate(2006,0)"></use><use data-c="1D41E" xlink:href="#MJX-22-TEX-B-1D41E" transform="translate(2964,0)"></use><use data-c="1D42D" xlink:href="#MJX-22-TEX-B-1D42D" transform="translate(3491,0)"></use><use data-c="1D42B" xlink:href="#MJX-22-TEX-B-1D42B" transform="translate(3938,0)"></use><use data-c="1D432" xlink:href="#MJX-22-TEX-B-1D432" transform="translate(4412,0)"></use></g></g></g></g></svg></mjx-container> — диференціальна геометрія.</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.439ex;" xmlns="http://www.w3.org/2000/svg" width="6.885ex" height="1.966ex" role="img" focusable="false" viewBox="0 -675 3043 869" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-23-TEX-B-1D413" d="M41 425Q41 426 51 545T62 669V675H737V669Q738 665 748 546T758 425V419H696V425Q687 517 669 555T595 607Q578 612 522 613H478V62H631V0H615Q585 3 399 3Q214 3 184 0H168V62H321V613H277H263Q164 613 134 561Q113 527 103 425V419H41V425Z"></path><path id="MJX-23-TEX-B-1D428" d="M287 -5Q228 -5 182 10T109 48T63 102T39 161T32 219Q32 272 50 314T94 382T154 423T214 446T265 452H279Q319 452 326 451Q428 439 485 376T542 221Q542 156 514 108T442 33Q384 -5 287 -5ZM399 230V250Q399 280 398 298T391 338T372 372T338 392T282 401Q241 401 212 380Q190 363 183 334T175 230Q175 202 175 189T177 153T183 118T195 91T215 68T245 56T287 50Q348 50 374 84Q388 101 393 132T399 230Z"></path><path id="MJX-23-TEX-B-1D429" d="M32 442L123 446Q214 450 215 450H221V409Q222 409 229 413T251 423T284 436T328 446T382 450Q480 450 540 388T600 223Q600 128 539 61T361 -6H354Q292 -6 236 28L227 34V-132H296V-194H287Q269 -191 163 -191Q56 -191 38 -194H29V-132H98V113V284Q98 330 97 348T93 370T83 376Q69 380 42 380H29V442H32ZM457 224Q457 303 427 349T350 395Q282 395 235 352L227 345V104L233 97Q274 45 337 45Q383 45 420 86T457 224Z"></path><path id="MJX-23-TEX-B-1D42C" d="M38 315Q38 339 45 360T70 404T127 440T223 453Q273 453 320 436L338 445L357 453H366Q380 453 383 447T386 403V387V355Q386 331 383 326T365 321H355H349Q333 321 329 324T324 341Q317 406 224 406H216Q123 406 123 353Q123 334 143 321T188 304T244 294T285 286Q305 281 325 273T373 237T412 172Q414 162 414 142Q414 -6 230 -6Q154 -6 117 22L68 -6H58Q44 -6 41 0T38 42V73Q38 85 38 101T37 122Q37 144 42 148T68 153H75Q87 153 91 151T97 147T103 132Q131 46 220 46H230Q257 46 265 47Q330 58 330 108Q330 127 316 142Q300 156 284 162Q271 168 212 178T122 202Q38 243 38 315Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D413" xlink:href="#MJX-23-TEX-B-1D413"></use><use data-c="1D428" xlink:href="#MJX-23-TEX-B-1D428" transform="translate(800,0)"></use><use data-c="1D429" xlink:href="#MJX-23-TEX-B-1D429" transform="translate(1375,0)"></use><use data-c="1D428" xlink:href="#MJX-23-TEX-B-1D428" transform="translate(2014,0)"></use><use data-c="1D42C" xlink:href="#MJX-23-TEX-B-1D42C" transform="translate(2589,0)"></use></g></g></g></g></svg></mjx-container> — теорія топосів.</p><p>Перелік теорем для самоверифікації: 1) Теорія чисел: Теорема про прості числа;
2) Фундаментальна теорема числення (аналіз);
3) Аналіз: Теорема про збіжність Лебега;
4) Топологія: Гіпотеза Пуанкаре (3D);
5) Алгебра: Класифікація скінченних простих груп;
6) Теорія множин: Незалежність гіпотези континууму (CH);
7) Теорія категорій: Теорема про спряжені функтори;
8) Гомотопічна теорія: Кон’юктура Адамса (через K-теорію);
9) Консистентність ZFC з великими кардиналами;
10) Остання теорема Ферма;
11) Теорема про великі кардинали: Максимум Мартіна.</p><p>Це не вичерпне, але оглядове бачення її здатності охоплювати алгебраїчні,
аналітичні, топологічні та фундаментальні домени. AXIO/1 є кандидатом на
універсальну механізовану математичну платформу, що конкурує з такими системами,
як кубічна теорія типів (Agda), чи індуктивна теорія типів з фактор-просторами (Lean),
розширюючи їхній обсяг примітивів.
</p></div><div class="om"><section><h1>Висновки</h1></section><p>Система AXIO/1 об’єднує синтетичні і класичні математики в механічно перевірюваній структурі.
Її категорні моделі охоплюють симпліціальні ∞-категорії, стабільні спектри,
когезивні модальності, ZFC, великі кардинали та форсинг, забезпечуючи повне
покриття математичних доменів станом на 2025 рік. Спектральна категорія мов
дозволяє працювати у внутрішніх мовах відповідних категорій і транспортувати
моделі за необхіодності у інші топоси для найефективніших обчислень, що робить систему
унікальною платформою для формалізації математик.
</p></div><div class="om"><section><h1>Публікації</h1><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol5/vol5.pdf">&nbsp; AXIO.PDF</a> Формальні Математики</div><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol3/henk.pdf">&nbsp; HENK.PDF</a> Хенк Барендрегт</div><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol1/mltt.pdf">&nbsp; MLTT.PDF</a> Пер Мартін-Льоф</div><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol3/anders.pdf">&nbsp; ANDERS.PDF</a> Андерс Мортберг</div><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol3/anders.pdf">&nbsp; LAURENT.PDF</a> Лоран Шварц</div><div style="padding-top: 8px;"><img src="https://anders.groupoid.space/images/pdf.jpg" width="35"><a href="https://groupoid.space/books/vol3/urs.pdf">&nbsp; URS.PDF</a> Урс Шрайбер</div></section></div></article><footer class="footer"><a href="https://5ht.co/license/"><img class="footer__logo" src="https://longchenpa.guru/seal.png" width="50"></a><span class="footer__copy">2016&mdash;2020 &copy; Дисертація <a rel="me" href="https://mathstodon.xyz/@5ht" style="color:white;"><u>Максима Сохацького</u></a></span><script src="https://groupoid.space/highlight.js"></script><script src="https://groupoid.space/bundle.js"></script></footer>