Интересные алгоритмы в формализации теоремы Фейта-Томпсона?

Похоже, Джордж Гонтье и его сотрудники закончили формализацию теоремы нечетного порядка .

В своей более ранней работе над теоремой о четырех цветах Гонтье изобрел кучу новых алгоритмов (в основном, вариантов BDD и графовых алгоритмов), которые были особенно пригодны для формальной проверки. Поскольку он сказал, что продолжал использовать этот метод проверки в мелкомасштабном отражении в работе над теорией конечных групп, мне интересно, какие новые алгоритмические приемы были разработаны в ходе этой разработки?

(Превращение комментария в ответ и его расширение)

От разговора с кем-то, кто работал над этим: нет. Он изобрел всевозможные умные уточнения многих доказательств и реструктурировал многие теоретические разработки, оба из которых чрезвычайно ценны, но задействованные алгоритмы не интересны - на самом деле, многие из них - тупая грубая сила, полная противоположность интересного.

По сути, то, что искали, - это прямая линия к доказательству Фейта Томпсона, не беспокоясь о «вычислительном содержании» на этом пути (и даже не слишком заботясь о возможности повторного использования некоторых модулей). Это было уже чрезвычайно амбициозно, учитывая сроки. К счастью, некоторые из людей, вовлеченных в проект, провели рефакторинг многих частей доказательств, которые будут

• более многоразовое использование для более широкого набора приложений
• более значимый в вычислительном отношении