I dunno what MKM should mean, but the table   
   of contents of the book below confirms my hypothesis   
      
   that many wish a better Computer Algebra System (CAS)   
   and Theorem Prover Assistant (TPA) integration.   
      
   Mining the Archive of Formal Proofs    
   Math Search for the Masses:    
   Multimodal Search Interfaces and Appearance Based Retrieval   
   Calculemus Towards Formal Fault Tree Analysis Using Theorem Proving   
   Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof   
   A First Class Boolean Sort in First-Order Theorem Proving and TPTP    
   Type Inference for ZFH   
   Generic Literals   
   Ranking/Unranking of Lambda Terms with Compressed de Bruijn Indices   
   Digital Mathematics Libraries: A Flexiformal Model of Knowledge    
   Dissemination and Aggregation in Mathematics   
   Mathematical Knowledge Management   
   Structure Formation in Large Theories   
   Formal Logic Definitions for Interchange Languages.   
   Math Literate Knowledge Management via Induced Material   
   Strategies for Parallel Markup   
   Readable Formalization of Euler’s Partition Theorem in Mizar   
   Automating Change of Representation for Proofs in Discrete Mathematics    
   Performance Evaluation and Optimization of Math-Similarity Search   
   Projects and Surveys   
   Mizar:State-of-the-Art and Beyond   
   Growing the Digital Repository of Mathematical Formulae with Generic LTX   
   Sources   
   Formalizing Physics: Automation, Presentation and Foundation Issues   
   A Surveyon Retrieval of Mathematical Knowledge   
   Towards the Formalization of Fractional Calculus in Higher-Order Logic   
   LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners   
   Systems and Data   
   TIP:Tons of Inductive Problems   
   Semantic Enrichment of Mathematics via ‘tooltips’   
   Documentation Generator Focusing on    
   Symbols for the HTML-ized Mizar Library    
   Tools for MML Environment Analysis    
   Enabling Symbolic and Numerical Computations in HOL Light   
   Erratum to: Towards Formal Fault Tree Analysis Using Theorem Proving   
      
   But all the above will be dust in the wind, if   
   not somebody pulls it in the style of Wolfram Alpha.   
      
   Am Sonntag, 29. Oktober 2017 01:56:43 UTC+2 schrieb Richard Fateman:   
   > but also look at MKM  , e.g.   
   > http://www.springer.com/de/book/9783319206141   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)