CV for Jesse Alama

A col­lec­tion of in­ter­views with dozens of Rack­et pro­gram­mers of their ex­pe­ri­ence of lan­guage-ori­ent­ed pro­gram­ming, of which Rack­et is a strong pro­po­nent.

A ten-chap­ter short course on ba­sic Rack­et pro­gram­ming.

A step-by-step guide to get­ting start­ed with the built-in Rack­et HTTP serv­er, with a sam­ple web ap­pli­ca­tion and its func­tion­al­i­ty built up in pieces. Sur­vey of a num­ber of third-par­ty li­braries that will prob­a­bly be used heav­i­ly by most web apps writ­ten in Rack­et.

An in­tro­duc­tion to the Snow­plow data an­a­lyt­ics and pipeline plat­form.

We out­line the rather com­pli­cat­ed his­to­ry of at­tempts at ax­iom­a­tiz­ing Jaśkows­ki's dis­cus­sive log­ic $\mathrm{D2}$ and show that some clar­i­ty can be had by pay­ing close at­ten­tion to the lan­guage we work with. We then ex­am­ine the prob­lem of ax­iom­a­tiz­ing $\mathrm{D2}$ in lan­guages in­volv­ing dis­cus­sive con­junc­tions. Specif­i­cal­ly, we show that re­cent at­tempts by Ciu­ciu­ra are mis­tak­en. Fi­nal­ly, we present an ax­iom­a­ti­za­tion of $\mathrm{D2}$ in the lan­guage Jaśkows­ki sug­gest­ed in his sec­ond pa­per on dis­cus­sive log­ic, by fol­low­ing a re­mark of da Cos­ta and Du­bika­jtis. We also deal with an in­ter­est­ing vari­ant of $\mathrm{D2}$, in­tro­duced by Ciu­ciu­ra, in which nega­tion is also tak­en to be dis­cus­sive.

We in­ves­ti­gate equa­tion­al the­o­ries ex­pressed in terms of the point-re­flec­tion op­er­a­tion \sig­ma and the mid­point op­er­a­tion $\mu$ that lie strict­ly be­tween the ab­solute and the affine the­o­ry, prov­ing a num­ber of de­pen­den­cies and in­de­pen­den­cies in the process. Sev­er­al uni­ver­sal the­o­ries en­larged with the collinear­i­ty pred­i­cate also lie strict­ly be­tween the ab­solute and the affine the­o­ry. The in­de­pen­dence mod­els and sev­er­al proofs were ob­tained by Tipi, an ag­gre­gate of au­to­mat­ic the­o­rem provers. To show that no set of equa­tions with at most three vari­ables can ax­iom­a­tize the affine the­o­ry is left as an open prob­lem.

Di­a­logue games are a two-play­er se­man­tics for a va­ri­ety of log­ics, in­clud­ing in­tu­ition­is­tic and clas­si­cal log­ic. Di­a­logues can be viewed as a kind of an­a­lyt­ic cal­cu­lus not un­like tableaux. Al­though di­a­logues can serve as an al­ter­na­tive char­ac­ter­i­za­tion of in­tu­ition­is­tic log­ic, it is less clear to what ex­tent di­a­logues can be prac­ti­cal­ly used as a search pro­ce­dure. We an­nounce Kuno, an au­to­mat­ed the­o­rem prover for in­tu­ition­is­tic first-or­der log­ic based on di­a­logue games.

Our com­pu­ta­tion­al meta­physics group de­scribes its use of au­to­mat­ed rea­son­ing tools to study Leib­niz's the­o­ry of con­cepts. We start with a re­con­struc­tion of Leib­niz's the­o­ry with­in the the­o­ry of ab­stract ob­jects (hence­forth ob­ject the­o­ry). Leib­niz's the­o­ry of con­cepts, un­der this re­con­struc­tion, has a non-modal al­ge­bra of con­cepts, a con­cept-con­tain­ment the­o­ry of truth, and a modal meta­physics of com­plete in­di­vid­ual con­cepts. We show how the ob­ject-the­o­ret­ic re­con­struc­tion of these com­po­nents of Leib­niz's the­o­ry can be rep­re­sent­ed for in­ves­ti­ga­tion by means of au­to­mat­ed the­o­rem provers and fi­nite mod­el builders. The fun­da­men­tal the­o­rem of Leib­niz's the­o­ry is de­rived us­ing these tools.

This is the trans­la­tion of the Mizar ar­ti­cle con­tain­ing read­able Mizar proofs of some ax­iomat­ic geom­e­try the­o­rems for­mu­lat­ed by the great Pol­ish math­e­mati­cian Al­fred Tars­ki, and we hope to con­tin­ue this work.

The ar­ti­cle is an ex­ten­sion and up­grad­ing of the source code writ­ten by the first au­thor with the help of miz3 tool; his pri­ma­ry goal was to use proof check­ers to help teach rig­or­ous ax­iomat­ic geom­e­try in high school us­ing Hilbert's ax­ioms.

This is large­ly a Mizar port of Julien Nar­boux's Coq pseu­do-code. We par­tial­ly prove the the­o­rem that Tars­ki's (ex­treme­ly weak!) plane geom­e­try ax­ioms im­ply Hilbert's ax­ioms. Specif­i­cal­ly, we ob­tain Gup­ta's amaz­ing proof which im­plies Hilbert's ax­iom I1 that two points de­ter­mine a line.

The pri­ma­ry Mizar cod­ing was heav­i­ly in­flu­enced by ax­ioms of in­ci­dence geom­e­try. The orig­i­nal de­vel­op­ment was much im­proved us­ing Mizar ad­jec­tives in­stead of pred­i­cates only, and to use this ma­chin­ery in full ex­tent, we have to con­struct some mod­els of Tars­ki geom­e­try. These are list­ed in the sec­ond sec­tion, to­geth­er with ap­pro­pri­ate reg­is­tra­tions of clus­ters. Also mod­els of Tars­ki's geom­e­try re­lat­ed to real planes were con­struct­ed.

Thanks to de­vel­op­ments in the last few decades in math­e­mat­i­cal log­ic and com­put­er sci­ence, it has now be­come pos­si­ble to for­mal­ize non-triv­ial math­e­mat­i­cal proofs in es­sen­tial­ly com­plete de­tail. we dis­cuss the philo­soph­i­cal prob­lems and prospects for such for­mal­iza­tion en­ter­pris­es. We show how some peren­ni­al philo­soph­i­cal top­ics and prob­lems in epis­te­mol­o­gy, phi­los­o­phy of sci­ence, and phi­los­o­phy of math­e­mat­ics can be seen in the prac­tice of for­mal­iz­ing math­e­mat­i­cal proofs.

Con­tem­po­rary ar­gu­men­ta­tion the­o­ry tends to steer away from tra­di­tion­al for­mal log­ic. In the case of ar­gu­men­ta­tion the­o­ry ap­plied to math­e­mat­ics, though, it is prop­er for ar­gu­men­ta­tion the­o­ry to re­vis­it for­mal log­ic ow­ing to the in-prin­ci­ple for­mal­iz­abil­i­ty of math­e­mat­i­cal ar­gu­ments. Com­plete­ly for­mal proofs of sub­stan­tial math­e­mat­i­cal ar­gu­ments suf­fer from well-known prob­lems. But prac­ti­cal for­mal­iza­tions of sub­stan­tial math­e­mat­i­cal re­sults are now avail­able, thanks to the help pro­vid­ed by mod­ern au­to­mat­ed rea­son­ing sys­tems. In-prin­ci­ple for­mal­iz­abil­i­ty has be­come in-prac­tice for­mal­iz­abil­i­ty. Such ef­forts are a re­source for ar­gu­men­ta­tion the­o­ry ap­plied to math­e­mat­ics be­cause top­ics that might be thought to be es­sen­tial­ly in­for­mal reap­pear in the com­put­er-as­sist­ed, for­mal set­ting, prompt­ing a fresh ap­praisal.

When for­mal­iz­ing proofs with proof as­sis­tants, it of­ten hap­pens that back­ground knowl­edge about math­e­mat­i­cal con­cepts is em­ployed with­out the for­mal­iz­er ex­plic­it­ly re­quest­ing it. Such mech­a­nisms are war­rant­ed in the con­text of dis­cov­ery be­cause they can make prover ses­sions more ef­fi­cient (less time search­ing the li­brary) and can com­press proofs (the more knowl­edge that is im­plic­it­ly avail­able, the less needs to be ex­plic­it­ly said by the for­mal­iz­er). In the con­text of jus­ti­fi­ca­tion, though, im­plic­it knowl­edge may need to be made ex­plic­it. To study im­plic­it knowl­edge in proof as­sis­tants, one must first char­ac­ter­ize what im­plic­it knowl­edge should be made ex­plic­it. Then, once a class of im­plic­it back­ground knowl­edge is iden­ti­fied, one needs to de­ter­mine how to ex­tract it from proofs. When a class of im­plic­it knowl­edge is made ex­plic­it, we may then in­quire to what ex­tent the im­plic­it knowl­edge is need­ed for any par­tic­u­lar proof; it of­ten hap­pens that proofs can be suc­cess­ful even if some of the im­plic­it knowl­edge is omit­ted. In this note we de­scribe an ex­per­i­ment con­duct­ed on the Mizar Math­e­mat­i­cal Li­brary (MML) of for­mal math­e­mat­i­cal proofs con­cern­ing a par­tic­u­lar class of im­plic­it back­ground knowl­edge, name­ly, prop­er­ties of func­tions and re­la­tions (e.g., com­mu­ta­tiv­i­ty, asym­me­try, etc.). In our ex­per­i­ment we sep­a­rate, for each the­o­rem of the MML, the need­ed func­tion and re­la­tion prop­er­ties from the un­need­ed ones. Spe­cial at­ten­tion is paid to those func­tion and re­la­tion prop­er­ties that are sig­nif­i­cant in dis­cus­sions of foun­da­tions of math­e­mat­ics.

De­pen­den­cies are iden­ti­fied in two re­cent­ly pro­posed first-or­der ax­iom sys­tems for plane hy­per­bol­ic geom­e­try. Since the de­pen­den­cies do not specif­i­cal­ly con­cern hy­per­bol­ic geom­e­try, our re­sults yield two sim­pler ax­iom sys­tems for ab­solute geom­e­try.

A re­cent­ly pro­posed ax­iom sys­tem for Andr´e's cen­tral trans­la­tion struc­tures is im­proved upon. First, one of its ax­ioms turns out to be de­pen­dent (de­riv­able from the oth­er ax­ioms). With­out this ax­iom, the ax­iom sys­tem is in­deed in­de­pen­dent. Sec­ond, where­as most of the orig­i­nal in­de­pen­dence mod­els were in­fi­nite, fi­nite in­de­pen­dence mod­els are avail­able. More­over, the in­de­pen­dence proof for one of the ax­ioms em­ployed proof-the­o­ret­ic tech­niques rather than in­de­pen­dence mod­els; for this ax­iom, too, a fi­nite in­de­pen­dence mod­el ex­ists. For every ax­iom, then, there is a fi­nite in­de­pen­dence mod­el. Fi­nal­ly, the ax­iom sys­tem (with­out its sin­gle de­pen­dent ax­iom) is not only in­de­pen­dent, but com­plete­ly in­de­pen­dent.

Di­a­logue se­man­tics for log­ic are two-play­er log­ic games be­tween a Pro­po­nent who puts for­ward a log­i­cal for­mu­la $\phi$ as valid or true and an Op­po­nent who dis­putes this. An ad­van­tage of the di­a­log­i­cal ap­proach is that it is a uni­form frame­work from which dif­fer­ent log­ics can be ob­tained through only small vari­a­tions of the ba­sic rules. We in­tro­duce the com­po­si­tion prob­lem for di­a­logue games as the prob­lem of re­solv­ing, for a set $S$ of rules for di­a­logue games, whether the set of $S$-di­a­log­i­cal­ly valid for­mu­las is closed un­der modus po­nens. Solv­ing the com­po­si­tion prob­lem is fun­da­men­tal for the di­a­log­i­cal ap­proach to log­ic; de­spite its sim­plic­i­ty, it of­ten re­quires an in­di­rect so­lu­tion with the help of sig­nif­i­cant log­i­cal ma­chin­ery such as cut-elim­i­na­tion. Di­rect so­lu­tions to the com­po­si­tion prob­lem can, how­ev­er, some­times be had. As an ex­am­ple, we give a set $N$ of di­a­logue rules which is well-jus­ti­fied from the di­a­log­i­cal point of view, but whose set $N$ of di­a­log­i­cal­ly valid for­mu­las is both non-triv­ial and non-stan­dard. We prove that the com­po­si­tion prob­lem for $N$ can be solved di­rect­ly, and in­tro­duce a tableaux sys­tem for $N$.

Di­a­logue games are a two-play­er game-based se­man­tics for a va­ri­ety of log­ics. The Pro­po­nent ($\mathrm{Pro}$) as­serts an ini­tial for­mu­la $\phi$; the Op­po­nent ($\mathrm{Opp}$) dis­putes that $\phi$ is valid. The play­ers take turns, at­tack­ing or de­fend­ing log­i­cal for­mu­las. There are a few ways in which di­a­logues can be de­fined. There seems to be no unique for­mal­iza­tion, though one can clear­ly see fam­i­ly re­sem­blances among them. One rule that comes up of­ten is the so-called $E$ rule, which says that $\mathrm{Opp}$ must re­spond to $\mathrm{Pro}$'s im­me­di­ate­ly pre­ced­ing move. The $E$ rule is re­gard­ed as awk­ward and lack­ing a clear sig­nif­i­cance in any or­di­nary sense of di­a­logue. Its sole val­ue ap­pears to be that it fa­cil­i­tates proofs of ad­e­qua­cy (sound­ness and com­plete­ness). While ac­knowl­edg­ing its util­i­ty, one might nat­u­ral­ly wish to elim­i­nate the $E$ rule, or at least re­place it by a rule that has in­tu­itive­ly greater plau­si­bil­i­ty. In some con­texts, it is known that $E$ is in fact re­dun­dant (a set of rules with $E$ has the same log­i­cal force as the rule­set with­out $E$), while in oth­er con­texts, $E$ seems to be es­sen­tial. To­ward that end, this note in­ves­ti­gates a di­a­log­i­cal char­ac­ter­i­za­tion of clas­si­cal log­ic in which the $E$ rule is re­laxed.

For a new­com­er, para­con­sis­tent log­ics can be dif­fi­cult to grasp. Even ex­perts in log­ic can find the con­cept of para­con­sis­ten­cy to be sus­pi­cious or mis­guid­ed, if not ac­tu­al­ly wrong. The prob­lem is that al­though they usu­al­ly have much in com­mon with more fa­mil­iar log­ics (such as in­tu­ition­is­tic or clas­si­cal log­ic), para­con­sis­tent log­ics nec­es­sar­i­ly dis­agree in oth­er parts of the log­i­cal ter­rain which one might have thought were not up for de­bate. Thus, one's log­i­cal in­tu­itions may need to be re­cal­i­brat­ed to work skill­ful­ly with para­con­sis­ten­cy. To get start­ed, one should clear­ly ap­pre­ci­ate the pos­si­bil­i­ty of para­con­sis­tent log­ics and the gen­uine­ness of the dis­tinc­tions to which para­con­sis­ten­cy points. For this pur­pose, one typ­i­cal­ly en­coun­ters ma­tri­ces in­volv­ing more than two truth val­ues to char­ac­ter­ize suit­able con­se­quence re­la­tions. In the eyes of a two-val­ued skep­tic, such an ap­proach might seem du­bi­ous. Even a non-skep­tic might won­der if there's an­oth­er way. To this end, to ex­plore the ba­sic no­tions of para­con­sis­tent log­ic with the as­sis­tance of au­to­mat­ed rea­son­ing tech­niques. Such an ap­proach has mer­it be­cause by del­e­gat­ing some of the log­i­cal work to a ma­chine, one's log­i­cal "bi­as­es" be­come ex­ter­nal­ized. The re­sult is a new way to ap­pre­ci­ate that the dis­tinc­tions to which para­con­sis­tent log­ic points are in­deed gen­uine. Our ap­proach can even sug­gest new ques­tions and prob­lems for the para­con­sis­tent log­ic com­mu­ni­ty.

We im­prove upon Hunt­ing­ton's affine geom­e­try by show­ing that his in­de­pen­dence proofs can be, in some cas­es, sim­pli­fied. We car­ry out a sys­tem­at­ic in­ves­ti­ga­tion of the strict no­tion of be­tween­ness that Hunt­ing­ton em­ploys (the three ar­gu­ments are sup­posed to be dis­tinct) by com­par­ing it to McPhee's three ax­iom sys­tems for the same in­tend­ed class of struc­tures, which em­ploys weak be­tween­ness (the ar­gu­ments are per­mit­ted to be equal). Upon close­ly in­spect­ing the proof that McPhee's ax­iom sys­tems are equiv­a­lent to Hunt­ing­ton's (sub­ject of course to the de­f­i­n­i­tion of weak be­tween­ness in terms of strict and vice ver­sa), one finds sur­pris­ing­ly that McPhee's ax­iom sys­tems have quite dif­fer­ent re­la­tions to strict be­tween­ness.

Smart premise se­lec­tion is es­sen­tial when us­ing au­to­mat­ed rea­son­ing as a tool for large-the­o­ry for­mal proof de­vel­op­ment. This work de­vel­ops learn­ing-based premise se­lec­tion in two ways. First, a fine-grained de­pen­den­cy analy­sis of ex­ist­ing high-lev­el for­mal math­e­mat­i­cal proofs is used to build a large knowl­edge base of proof de­pen­den­cies, pro­vid­ing pre­cise data for ATP-based re-ver­i­fi­ca­tion and for train­ing premise se­lec­tion al­go­rithms. Sec­ond, a new ma­chine learn­ing al­go­rithm for premise se­lec­tion based on ker­nel meth­ods is pro­posed and im­ple­ment­ed. To eval­u­ate the im­pact of both tech­niques, a bench­mark con­sist­ing of 2078 large-the­o­ry math­e­mat­i­cal prob­lems is con­struct­ed, ex­tend­ing the old­er MPTP Chal­lenge bench­mark. The com­bined ef­fect of the tech­niques re­sults in a 50 % im­prove­ment on the bench­mark over the state-of-the-art Vam­pire/SInE sys­tem for au­to­mat­ed rea­son­ing in large the­o­ries.

In some the­o­ry de­vel­op­ment tasks, a prob­lem is sat­is­fac­to­ri­ly solved once it is shown that a the­o­rem (con­jec­ture) is de­riv­able from the back­ground the­o­ry (premis­es). De­pend­ing on one's mo­ti­va­tions, the de­tails of the de­riva­tion of the con­jec­ture from the premis­es may or may not be im­por­tant. In some con­texts, though, one wants more from the­o­ry de­vel­op­ment than sim­ply de­riv­abil­i­ty of the tar­get the­o­rems from the back­ground the­o­ry. One may want to know which premis­es of the back­ground the­o­ry were used in the course of a proof out­put by an au­to­mat­ed the­o­rem prover (when a proof is avail­able), whether they are all, in suit­able sens­es, nec­es­sary (and why), whether al­ter­na­tive proofs can be found, and so forth. The prob­lem, then, is to sup­port proof analy­sis in the­o­ry de­vel­op­ment; the tool de­scribed in this pa­per, Tipi, aims to pro­vide pre­cise­ly that.

First-or­der trans­la­tions of large math­e­mat­i­cal repos­i­to­ries al­low dis­cov­ery of new proofs by au­to­mat­ed rea­son­ing sys­tems. Large amounts of avail­able math­e­mat­i­cal knowl­edge can be re-used by com­bined AI/ATP sys­tems, pos­si­bly in un­ex­pect­ed ways. But au­to­mat­ed sys­tems can be also more eas­i­ly mis­led by ir­rel­e­vant knowl­edge in this set­ting, and find­ing deep­er proofs is typ­i­cal­ly more dif­fi­cult. Both large-the­o­ry AI/ATP meth­ods, and trans­la­tion and data-min­ing tech­niques of large for­mal cor­po­ra, have sig­nif­i­cant­ly de­vel­oped re­cent­ly, pro­vid­ing enough data for an ini­tial com­par­i­son of the proofs writ­ten by math­e­mati­cians and the proofs found au­to­mat­i­cal­ly. This pa­per de­scribes such an ini­tial ex­per­i­ment and com­par­i­son con­duct­ed over the 50000 math­e­mat­i­cal the­o­rems from the Mizar Math­e­mat­i­cal Li­brary.

We an­nounce a tool for map­ping de­riva­tions pro­duced by the E the­o­rem prover to Mizar proofs. Our map­ping com­ple­ments ear­li­er work that gen­er­ates prob­lems for au­to­mat­ed the­o­rem provers from Mizar in­fer­ence check­ing prob­lems. We de­scribe the tool, ex­plain the map­ping, and show how we solved some of the dif­fi­cul­ties that arise in map­ping proofs be­tween dif­fer­ent log­i­cal for­malisms, even when they are based on the same no­tion of log­i­cal con­se­quence, as Mizar and E are (name­ly, first-or­der clas­si­cal log­ic with iden­ti­ty).

The Mizar lan­guage aims to cap­ture math­e­mat­i­cal ver­nac­u­lar by pro­vid­ing a rich lan­guage for math­e­mat­ics. From the per­spec­tive of a user, the rich­ness of the lan­guage is wel­come be­cause it makes writ­ing texts more "nat­ur­al". But for the de­vel­op­er, the rich­ness leads to syn­tac­tic com­plex­i­ty, such as deal­ing with over­load­ing.

Re­cent­ly the Mizar team has been mak­ing a fresh ap­proach to the prob­lem of pars­ing the Mizar lan­guage. One aim is to make the lan­guage ac­ces­si­ble to users and oth­er de­vel­op­ers. In this pa­per we de­scribe these new pars­ing ef­forts and some ap­pli­ca­tions there­of, such as large-scale text refac­tor­ings, pret­ty-print­ing, HTTP pars­ing ser­vices, and nor­mal­iza­tions of Mizar texts.

Two meth­ods for ex­tract­ing de­tailed for­mal de­pen­den­cies from the Coq and Mizar sys­tem are pre­sent­ed and com­pared. The meth­ods are used for de­pen­den­cy ex­trac­tion from two large math­e­mat­i­cal repos­i­to­ries: the Coq Repos­i­to­ry at Ni­jmegen and the Mizar Math­e­mat­i­cal Li­brary. Sev­er­al ap­pli­ca­tions of the de­tailed de­pen­den­cy analy­sis are de­scribed and pro­posed. Mo­ti­vat­ed by the dif­fer­ent ap­pli­ca­tions, we dis­cuss the var­i­ous kinds of de­pen­den­cies that we are in­ter­est­ed in, and the suit­abil­i­ty of var­i­ous de­pen­den­cy ex­trac­tion meth­ods.

In re­cent years wikis for for­mal math­e­mat­ics have ap­peared. For­mal math­e­mat­ics presents a num­ber of chal­lenges for the wiki per­spec­tive. To en­hance the qual­i­ty of the data in these wikis from the per­spec­tive of in­for­ma­tion ar­chi­tec­ture, we pro­pose some ex­ten­sions of ex­ist­ing for­mal math­e­mat­ics wikis to more prop­er­ly han­dle meta­da­ta.

We present sev­er­al steps to­wards large for­mal math­e­mat­i­cal wikis. The Coq proof as­sis­tant to­geth­er with the CoRN repos­i­to­ry are added to the pool of sys­tems han­dled by the gen­er­al wiki sys­tem de­scribed in [10]. A smart re-ver­i­fi­ca­tion scheme for the large for­mal li­braries in the wiki is sug­gest­ed for Mizar/MML and Coq/CoRN, based on re­cent­ly de­vel­oped pre­cise track­ing of math­e­mat­i­cal de­pen­den­cies. We pro­pose to use fea­tures of state-of-the-art filesys­tems to al­low real-time cloning and sand­box­ing of the en­tire li­braries, al­low­ing also to ex­tend the wiki to a true mul­ti-user col­lab­o­ra­tive area. A num­ber of re­lat­ed is­sues are dis­cussed.

The MML is one of the largest col­lec­tion of for­mal­ized math­e­mat­i­cal knowl­edge that has been de­vel­oped with var­i­ous in­ter­ac­tive proof as­sis­tants. It com­pris­es more than 1100 "ar­ti­cles" sum­ming to near­ly 2.5 mil­lion lines of text, each con­sist­ing of a uni­fied col­lec­tion of math­e­mat­i­cal de­f­i­n­i­tions and proofs. Se­man­ti­cal­ly, it con­tains more than 50000 the­o­rems and more than 10000 de­f­i­n­i­tions ex­pressed us­ing more than 7000 sym­bols. It thus of­fers a fas­ci­nat­ing cor­pus on which one could car­ry out a num­ber of ex­per­i­ments. This note dis­cuss­es a sys­tem for com­put­ing fine-grained de­pen­den­cies among the con­tents of the MML.

The Mizar Math­e­mat­i­cal Li­brary (MML) is a large cor­pus of for­malised math­e­mat­i­cal knowl­edge. It has been con­struct­ed over the course of many years by a large num­ber of au­thors and main­tain­ers. Yet the le­gal sta­tus of these ef­forts of the Mizar com­mu­ni­ty has nev­er been clar­i­fied. In 2010, af­ter many years of loose de­lib­er­a­tions, the com­mu­ni­ty de­cid­ed to in­ves­ti­gate the is­sue of li­cens­ing the con­tent of the MML, there­by clar­i­fy­ing and crys­tal­liz­ing the sta­tus of the texts, the text's au­thors, and the li­brary's long-term main­tain­ers. The com­mu­ni­ty has set­tled on a copy­right and li­cense pol­i­cy that suits the pe­cu­liar fea­tures of Mizar and its com­mu­ni­ty. In this pa­per we dis­cuss the copy­right and li­cense so­lu­tions. We of­fer our ex­pe­ri­ence in the hopes that the com­mu­ni­ties of oth­er li­braries of for­malised math­e­mat­i­cal knowl­edge might take up the le­gal and sci­en­tif­ic prob­lems that we ad­dressed for Mizar.

We de­fine a class of di­a­logue games and prove that ex­is­tence of win­ning strate­gies for the Pro­po­nent in this class of games cor­re­sponds to va­lid­i­ty in clas­si­cal propo­si­tion­al log­ic. Many au­thors have stat­ed sim­i­lar re­sults with­out ac­tu­al­ly prov­ing the cor­re­spon­dence. We mod­i­fy the games used for in­tu­ition­is­tic log­ic giv­en by Fer­müller. We em­ploy stan­dard di­a­logue games and a stan­dard se­quent cal­cu­lus for clas­si­cal log­ic. The re­sult is a sim­ple cor­re­spon­dence be­tween di­a­logue games and clas­si­cal log­ic.

For­mal math­e­mat­ics has so far not tak­en full ad­van­tage of ideas from col­lab­o­ra­tive tools such as wikis and dis­trib­uted ver­sion con­trol sys­tems (DVCS). We ar­gue that the field could prof­it from such tools, serv­ing both new­com­ers and ex­perts alike. We de­scribe a pre­lim­i­nary sys­tem for such col­lab­o­ra­tive de­vel­op­ment based on the Git DVCS. We fo­cus, ini­tial­ly, on the Mizar sys­tem and its li­brary of for­mal­ized math­e­mat­ics.

This note re­ports on some ex­per­i­ments, us­ing a hand­ful of stan­dard au­to­mat­ed rea­son­ing tools, for ex­plor­ing Steinitz-Rademach­er poly­he­dra, which are mod­els of a cer­tain first-or­der the­o­ry of in­ci­dence struc­tures. This the­o­ry and its mod­els, even sim­ple ones, presents sig­nif­i­cant, geo­met­ri­cal­ly fas­ci­nat­ing chal­lenges for au­to­mat­ed rea­son­ing tools.

Euler's poly­he­dron for­mu­la as­serts for a poly­he­dron $p$ that $V-E+F=2$, where $V$, $E$, and $F$ are, re­spec­tive­ly, the num­bers of ver­tices, edges, and faces of $p$. Mo­ti­vat­ed by I. Lakatos's phi­los­o­phy of math­e­mat­ics as pre­sent­ed in his Proofs and Refu­ta­tions, in which the his­to­ry of Euler's for­mu­la is used as a case study to il­lus­trate Lakatos's views, we for­mal­ized a proof of Euler's for­mu­la for­mu­la in the Mizar sys­tem. We de­scribe some of the no­table fea­tures of the proof and sketch an im­proved for­mal­iza­tion in progress that takes a deep­er math­e­mat­i­cal per­spec­tive, us­ing the ba­sic re­sults of al­ge­bra­ic topol­o­gy, than the ini­tial for­mal­iza­tion did.

Euler's poly­he­dron for­mu­la as­serts for a poly­he­dron $p$ that $V-E+F=2$, where $V$ , $E$, and $F$ are, re­spec­tive­ly, the num­bers of ver­tices, edges, and faces of $p$. This pa­per con­cerns a for­mal proof in the mizar sys­tem of Euler's poly­he­dron for­mu­la car­ried out by the au­thor. We dis­cuss the in­for­mal proof (Poin­caré's) on which the for­mal proof is based, the for­mal­ism in which the proof was car­ried out, no­table fea­tures of the for­mal­iza­tion, and re­lat­ed projects.

Euler's poly­he­dron the­o­rem states for a poly­he­dron p, that $V-E+F=2$, where $V$, $E$, and $F$ are, re­spec­tive­ly, the num­ber of ver­tices, edges, and faces of $p$. The for­mu­la was first stat­ed in print by Euler in 1758. The proof giv­en here is based on Poin­caré's lin­ear al­ge­bra­ic proof, as adapt­ed by Imre Lakatos in the lat­ter's Proofs and Refu­ta­tions.

As is well known, Euler's for­mu­la is not true for all poly­he­dra. The con­di­tion on poly­he­dra con­sid­ered here is that of be­ing a ho­mol­o­gy sphere, which says that the cy­cles (chains whose bound­ary is zero) are ex­act­ly the bound­ing chains (chains that are the bound­ary of a chain of one high­er di­men­sion).

The present proof ac­tu­al­ly goes be­yond the three-di­men­sion­al ver­sion of the poly­he­dral for­mu­la giv­en by Lakatos; it is di­men­sion-free, in the sense that it gives a for­mu­la in which the di­men­sion of the poly­he­dron is a pa­ra­me­ter. The clas­si­cal Euler re­la­tion $V-E+F=2$ is cor­re­sponds to the case where the di­men­sion of the poly­he­dron is $3$.

The main the­o­rem, ex­pressed in the lan­guage of the present ar­ti­cle, is

$$Sum\text{al­ter­nat­ing−char­ac­ter­is­tic−se­quence}\left(p\right)=0\text{,}$$

where $p$ is a poly­he­dron. The al­ter­nat­ing char­ac­ter­is­tic se­quence of a poly­he­dron is the se­quence

$$-N_{\mathrm{-1}}\text{,}+N_0\text{,}-N_1\text{, …,}{\mathrm{-1}}^{dimp}\times N_{dimp}\text{,}$$

where $N_k$ is the num­ber of poly­topes of $p$ of di­men­sion $k$. The spe­cial case of $dimp=3$ yields Euler's clas­si­cal re­la­tion. ($N_{\mathrm{-1}}$ and $N_3$ will turn out to be equal, by de­f­i­n­i­tion, to $1$.)

Two oth­er spe­cial cas­es are proved: the first says that a one-di­men­sion­al poly­he­dron that is a ho­mol­o­gy sphere con­sists of just two ver­tices (and thus con­sists of just a sin­gle edge); the sec­ond spe­cial case as­serts that a two-di­men­sion­al poly­he­dron that is a ho­mol­o­gy sphere (a poly­gon) has as many ver­tices as edges.

For each set $X$, the pow­er set of $X$ forms a vec­tor space over the field $Z_2$ (the two-el­e­ment field $\left\{0\text{,}1\right\}$ with ad­di­tion and mul­ti­pli­ca­tion done mod­u­lo $2$): vec­tor ad­di­tion is dis­joint union, and scalar mul­ti­pli­ca­tion is de­fined by the two equa­tions ($1·x:=x$, $0·x:=\text{∅}$ for sub­sets $x$ of $X$).

The rank+nul­li­ty the­o­rem states that, if $T$ is a lin­ear trans­for­ma­tion from a fi­nite-di­men­sion­al vec­tor space $V$ to a fi­nite-di­men­sion­al vec­tor space $W$, then $dimV=rankT+nul­li­tyT$, where $rankT=dimimT$ and $nul­li­tyT=dimkerT$. The proof treat­ed here is stan­dard: take a ba­sis $A$ of $kerT$ and ex­tend it to a ba­sis $B$ of $V$, and then show that $dimimT$ is equal to $|B-A|$, and that $T$ is one-to-one on $B-A$.