D6.10: Towards Mathematical Data as VRE components

[minrk]

• WP6: Data/Knowledge/Software-Bases
• Lead Institution: FAU
• Due: 2019-08-31 (month 48; postponed from M42 in the last amendment)
• Nature: Other
• Task: T6.10 (#132), T6.11 (#286)
• Proposal: p.54
• Final report (sources)

This report summarizes the achievements in Work Package 6 over the last year of the OpenDreamKit project. Namely it covers results of T6.10: Math Search Engine and T6.11: Isabelle Case Study and tasks T6.6-6.8 (case studies in mathematical data sets).

In the last year, significant progress has been made in four areas:

• the understanding of D/K/S-bases: we have codified the experiences in the OpenDreamKit project into a tetrapodal view on "doing mathematics", which extends the Data/Knowledge/Software model of the proposal by "narration" and "organization" aspects.
• the Knowledge (K) aspect, where we have developed an exporter from library the Isabelle Theorem prover (Archive of Formal Proof) to an extensive RDF triple store, which can be queried by standard SPARQL queries for semantic search.
• the data (D) aspect, where we have
  • developed both an innovative model of (deep) FAIR in mathematics (and have integrated it with the MitM paradigm developed in OpenDreamKit),
  • have implemented in a prototypical system (data.mathhub), and have
  • evaluated it on the mathematical community outside the core OpenDreamKit community.
• computational mathematical documents (the S aspect of D/K/S or the "narration" and "computation" aspects of the finer tetrapod model). Here we have developed a formula harvester for jupyter notebooks and a formula search engine that builds on them (as envisioned in task T10 of WP6).

Note: The title of this deliverable was originally entitled Full-text search (Formulae + Keywords) in OpenDreamKit. However, in the last grant agreement amendment, the scope was broadened to a report on the remaining WP6 activities and achievements -- also to account for the new task T6.11. The title was changed to better reflect the actual content which, beyond Full-text search, targets the integration of mathematical data in Virtual Research Environments.

[bpilorget]

#140 was merged into #134 after the 3rd amendment to the contract

[nthiery]

We discussed this deliverable in length with @kohlhase, @florian-rabe, @tkw1536, and have a fairly specific plan. The KWARC team will be working on it in the coming days. A stub report file is now available; see the source link above.

[florian-rabe]

As discussed, I've integrated two of our recent papers into the report.

@kohlhase Can you make the next pass?
I merged the two introductions and conclusions and wrote some glue text.
In the Isabelle section, I merged multiple papers, and that should be reread in particular.
In the data section, I used only the journal paper - maybe @katjabercic can add some text from the longer conference paper, especially some screenshots regarding search.

[kohlhase]

I will do that.

[kohlhase]

I have added an abstract in the WP issue. Please have a look. I will copy this into the report for now, so that it can be further developed there. We may have to synchronize the two at the end.

[kohlhase]

@nthiery We should probably ask the project officer whether we can change the title into something more meaningful, to make it more accessible to the reviewers and the outside community.

[kohlhase]

I have written a first introduction. I think this should work. @florian-rabe please have a look.

[kohlhase]

I have written the general text for the conclusion @florian-rabe please re-read.

STATE: When the contributions from @tkw1536 and @katjabercic are complete, we should be almost done. I am meeting with both of them today to sync.

[kohlhase]

@mtorpey the conclusion of D6.10 touches on persistent memoization and I have attempted an evaluation wrt. data sets in the last paragraph of the conclusion. Please re-read and correct/improve/discuss.

[kohlhase]

Oh, and there are two ednotes for @florian-rabe about sizes.

[florian-rabe]

There is still one issue with the screenshots, which are currently for a Coq query. I had asked @Jazzpirate if he can switch them for Isabelle screenshots but have not heard back yet.
If not, we may need to rewrite the text a bit to explain that.

I have written the general text for the conclusion @florian-rabe please re-read.

Revised.

Oh, and there are two ednotes for @florian-rabe about sizes.

Done.

[kohlhase]

I have changed the title, and Tom and Katja are on the final changes to their sections.
Also Dennis is on the screenshots.
I expect things to converge to "ready to submit" by 14:00.

[embray]

"Concretely, this report reports on"

the repetition there is a bit jarring, at least in English. Maybe just synonym like "this report expounds on" or even just strike "report" since it's clear from the previous sentence.

[kohlhase]

you are right, could you please correct?

[kohlhase]

Dennis has supplied new screenshots; one issue down, two to go.

[embray]

Some of that wording came from the GitHub issue description, so that will have to be edited, and re-downloaded or edited directly when re-compiling the PDF.

[kohlhase]

I have to go now (and will be possibly offline from now on)
The report is ready for publication except for some text/diagram updates from @tkw1536 and @katjabercic (and the issue synchronization).

I am turning over the lead on this to @katjabercic and @florian-rabe who will do the end redaction and tell Nicolas when all is ready.

[katjabercic]

Some of that wording came from the GitHub issue description, so that will have to be edited, and re-downloaded or edited directly when re-compiling the PDF.

@embray if this just means you made some changes to the issue/latex but not the other, could you propagate the change?

If that is not the case, could you elaborate?

[nthiery]

Thank you Michael for leading this gracefully! Will submit upon notice.

[nthiery]

I updated the github issue description to handle Erik's suggestion and review the piece about title change. I will update the copy in the repo when I'll submit.

[katjabercic]

@nthiery D6.10 is as ready as it will be!

[embray]

I am making a few last second typo fixes from my proofreading. Hang tight.

[embray]

In the sentence

Schematic variables are renamed to fresh free variables. Since schematic variables are morally
like a universal quantifier prefix, this preserves the logical meaning of a formala (e.g. a theorem
statement).

Is "formala" meant to read "formula", or is it an intentionally "made up" (as far as I can tell) word relating to some formal entity of some kind?

[embray]

I can't tell if the parenthetical in this sentence is a typo or not:

Only the head statement of a theorem is considered, its
proof body remains abstract (as reference Isar to proof text).

I know "Isar" is a valid term here but the wording doesn't make sense to me.

[florian-rabe]

@embray Both were typos. I fixed them.

[embray]

@florian-rabe Thank you!

[nthiery]

Time to celebrate!
Thanks everyone for this nice piece of work, and the very timely reporting:-)