More fixes

Proposal/WorkPackages/Cases.tex

@@ -38,9 +38,9 @@ The Open Archive of Formalizations (OAF) is a collection of proof assistant libr
 This includes specifying their semantics in the format itself via meta-logics.
 
 In this task we complete the conversion and convert them into the \TheProject standard format.
-In particular, the representation of proofs will be very challenging.
-Moreover, each proof assistant library is a difficult very conversion task by itself because each uses a different, very complex meta-logic.
-Therefore, we will only be pick very few proof assistant libraries as examples.
+In particular, the representation of proofs will be challenging.
+Moreover, each proof assistant library is a difficult conversion task by itself because each uses a different, complex meta-logic.
+Therefore, we will only be pick few proof assistant libraries as examples.
 
 This task will be led by \site{FAU}, which has already built the OAF.
 \end{task}

Proposal/WorkPackages/DisseminationCommunityBuilding.tex

@@ -15,7 +15,7 @@
   \end{inparaenum}
   This includes:
   \begin{compactitem}
-  \item ensuring awareness of the results in the user community
+  \item ensuring awareness of the results in the user community,
   \item engaging cross communities discussions to foster scientific collaboration and conjoint development,
   \item spreading the expertise through workshops and training sessions,
   \item providing training for dataset developers how to make their datasets more visible.
@@ -108,7 +108,7 @@ PM=12,partners={CAE,CHA,FAU,FIZ,UL,PS}]
 In this task, we conduct general outreach activities targeted at researchers and industry practitioners.
 These will take the form of official communications, workshops at major mathematical meetings, and targeted communications to  specific communities.
 This includes transdisciplinary outreach to related fields that involve mathematical data, in particular computer science, physics, life sciences, and engineering.
-We will build on existing research communities connected with the partners, such as the more than 2,000 individual EMS members or more than 7,000 zbMATH reviewers. APIs designed for specific community needs will propel the adaptation of the services further. As a model serves, e.g., the open zbMATH API for the MathOverflow community site \cite{MO:on}, which is currently the largest online community in mathematics ($\approx 90 K$ registered users). A lean API facilitates the integration of references into the discussed questions there, and allows vice versa for the seamless interlinking of the literature with ongoing research. Similar advantages can be expected from availability of research data. Beyond mathematics, this task will be synergistically supported by the system APIs to RADAR research data hosting service provided by \site{FIZ}: researchers from other domains can host their research data on RADAR and integrate mathematical aspects into the \pn framework. The expertise developed in \TheProject on standardization and dissemination of symbolic data resources will fed into FORCE11 community standards like previously for software standardization.
+We will build on existing research communities connected with the partners, such as the more than 2,000 individual EMS members or more than 7,000 zbMATH reviewers. APIs designed for specific community needs will propel the adaptation of the services further. As a model serves, e.g., the open zbMATH API for the MathOverflow community site~\cite{MO:on}, which is currently the largest online community in mathematics ($\approx 90 K$ registered users). A lean API facilitates the integration of references into the discussed questions there, and allows vice versa for the seamless interlinking of the literature with ongoing research. Similar advantages can be expected from availability of research data. Beyond mathematics, this task will be synergistically supported by the system APIs to RADAR research data hosting service provided by \site{FIZ}: researchers from other domains can host their research data on RADAR and integrate mathematical aspects into the \pn framework. The expertise developed in \TheProject on standardization and dissemination of symbolic data resources will fed into FORCE11 community standards like previously for software standardization.
 
 This task will be led by \site{EMS}, which has the institutional support and recognition to conduct formal outreach activities.
 All other sites will contribute.