Proph Voevodsky

https://1337777.github.io/init.html

solves some question of Bertot [fn:1] which is how to communicate COQ math programming. Some finding is that the information-technology enabled by the _EMACS org-mode_ [fn:2] logiciel is effective to communicate _timed-synchronized_ _geolocated_ _simultaneously-edited_ _multi-authors_ _searchable_ text, and therefore to communicate textual COQ math programming.

For instance, the wiki-style https://github.com/1337777/1337777.github.io is the output of some automated _continuous-integration_ (periodic-pull, make emacs org, make coq, push) bash script [fn:3] which shall periodically input changes from everybody ( merge-conflict seniority-sorted ... ) github-repositories if it is by-chance named « OOO1337777 » . Some corresponding logiciel [fn:4] [fn:5] shall enable webcitations / reviews.

Memo that the common writing of mathematics using /vertically stacked/ symbols or /large/ symbols is mostly not necessary both from the prettiness angle of view ( /.PDF obsession/ ) or from the sensible-encoding angle of view. In this sense, the combination of all the techniques of the COQ computer and the SSREFLECT style is sufficient to do mathematics at least at the most-meta encoding ( /temporal-deductions by the bio-memory/ ).

This angle of view also solves some question of templetonworldcharity.org [fn:6] which is how information(-technology) enables the communication of discoveries with the motivation of affecting permanent impact : onto both the scholarly class and the wider public , by both the predictable logical method and the dia-para-logical randomness of reality .


[fn:1] ~Bertot~
[[https://team.inria.fr/marelle/advanced-coq-winter-school-2016-2017/]]
[fn:2] [[http://alan.petitepomme.net/tips/executing_coq.html]]
[fn:3] ~1337777.OOO~ [[https://github.com/1337777/OOO1337777/blob/master/makegit.sh.org]]
[fn:4] ~1337777.OOO~ [[http://1337777.link/ooo/guJAH-jSeQcTEST/2016/1/5/11/9/11/1]]
[fn:5] ~1337777.OOO~ [[https://github.com/1337777/upo/blob/master/editableTree.urp]]
[fn:6] [[http://www.templetonworldcharity.org/what-we-fund/core-funding-areas/big-questions]]