J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze, and J. Urban, Premise Selection for Mathematics by Corpus Analysis and Kernel Methods, Journal of Automated Reasoning, vol.50, issue.1???2, pp.191-213, 2014.
DOI : 10.1007/s10817-013-9286-5

J. Alama, D. Kühlwein, and J. Urban, Automated and Human Proofs in General Mathematics: An Initial Comparison, LPAR-18, pp.37-45, 2012.
DOI : 10.1007/978-3-642-28717-6_6

S. Berghofer and T. Nipkow, Proof Terms for Simply Typed Higher Order Logic, LNCS, vol.1869, pp.38-52, 2000.
DOI : 10.1007/3-540-44659-1_3

J. Christian-blanchette, S. Böhme, M. Fleury, S. J. Smolka, and A. Steckermeier, Semi-intelligible Isar proofs from machine-generated proofs, J. Autom. Reasoning

J. Christian-blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, Journal of Automated Reasoning, vol.13, issue.5, pp.109-128, 2013.
DOI : 10.1007/s10817-013-9278-5

J. Christian-blanchette, S. Böhme, A. Popescu, and N. Smallbone, Encoding monomorphic and polymorphic types, TACAS 2013, pp.493-507, 2013.

J. Christian-blanchette, A. Popescu, D. Wand, and C. Weidenbach, More SPASS with Isabelle?Superposition with hard sorts and configurable simplification, ITP 2012, pp.345-360, 2012.

S. Böhme and T. Nipkow, Sledgehammer: Judgement Day, IJCAR 2010, pp.107-121, 2010.
DOI : 10.1007/978-3-642-14203-1_9

T. Bouton, D. Caminha, B. De-oliveira, D. Déharbe, and P. Fontaine, veriT: An Open, Trustable and Efficient SMT-Solver, LNCS, vol.144, issue.2, pp.151-156, 2009.
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634

L. De, M. , and N. Bjørner, Z3: An efficient SMT solver, LNCS, vol.4963, pp.337-340, 2008.

J. Denzinger, M. Fuchs, C. Goller, and S. Schulz, Learning from previous proof experience, 1999.

T. Gauthier and C. Kaliszyk, Premise Selection and External Provers for HOL4, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP '15, pp.49-57, 2015.
DOI : 10.1145/2676724.2693173

A. Grabowski, A. Korni?owicz, and A. Naumowicz, Mizar in a nutshell, J. Formalized Reasoning, vol.3, issue.2, pp.153-245, 2010.

D. Greenaway, J. Andronick, and G. Klein, Bridging the Gap: Automatic Verified Abstraction of C, ITP 2012, pp.99-115, 2012.
DOI : 10.1007/978-3-642-32347-8_8

C. Thomas and . Hales, Introduction to the Flyspeck project, Mathematics, Algorithms, Proofs, number 05021 in Dagstuhl Seminar Proceedings Internationales Begegnungs-und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, pp.1-11, 2006.

J. Harrison, . Hol, and . Light, A tutorial introduction, FMCAD '96, pp.265-269, 1996.

J. Heras, E. Komendantskaya, M. Johansson, and E. Maclean, Proof-Pattern Recognition and Lemma Discovery in ACL2, LNCS, vol.8312, issue.19, pp.389-406, 2013.
DOI : 10.1007/978-3-642-45221-5_27

K. Hoder and A. Voronkov, Sine Qua Non for Large Theory Reasoning, LNCS, vol.37, issue.1-2, pp.299-314, 2011.
DOI : 10.1007/978-3-642-15582-6_30

J. Hölzl and A. Heller, Three chapters of measure theory in Isabelle/HOL, LNCS, vol.6898, pp.135-151, 2011.

J. Hurd, First-order proof tactics in higher-order logic theorem provers, Design and Application of Strategies/Tactics in Higher Order Logics, NASA Tech. Reports, pp.56-68, 2003.

K. Spärck and J. , A STATISTICAL INTERPRETATION OF TERM SPECIFICITY AND ITS APPLICATION IN RETRIEVAL, Journal of Documentation, vol.28, issue.1, pp.11-21, 1972.
DOI : 10.1108/eb026526

C. Kaliszyk and J. Urban, Stronger automation for Flyspeck by feature weighting and strategy evolution, PxTP 2013, pp.87-95, 2013.

C. Kaliszyk and J. Urban, Learning-Assisted Automated Reasoning with Flyspeck, Journal of Automated Reasoning, vol.50, issue.1???2, pp.173-213, 2014.
DOI : 10.1007/s10817-014-9303-3

C. Kaliszyk and J. Urban, HOL(y)Hammer: Online ATP Service for HOL Light, Mathematics in Computer Science, vol.50, issue.1, pp.5-22, 2015.
DOI : 10.1007/s11786-014-0182-0
URL : http://arxiv.org/abs/1309.4962

C. Kaliszyk and J. Urban, MizAR 40 for Mizar 40, Journal of Automated Reasoning, vol.50, issue.1-2, pp.245-256, 2015.
DOI : 10.1007/s10817-015-9330-8

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock et al., seL4, Communications of the ACM, vol.53, issue.6, pp.53107-115, 2010.
DOI : 10.1145/1743546.1743574

G. Klein and T. Nipkow, Jinja is not Java, Archive of Formal Proofs, 2005.

G. Klein, T. Nipkow, and L. Paulson, Archive of Formal Proofs

L. Kovács and A. Voronkov, First-Order Theorem Proving and Vampire, CAV 2013, pp.1-35, 2013.
DOI : 10.1007/978-3-642-39799-8_1

D. Kuehlwein and J. Urban, Learning from multiple proofs: First experiments, EPiC, vol.21, pp.82-94, 2013.

D. Kühlwein, J. C. Blanchette, C. Kaliszyk, and J. Urban, MaSh: Machine Learning for Sledgehammer, ITP 2013, pp.35-50, 2013.
DOI : 10.1007/978-3-642-39634-2_6

D. Kühlwein, E. Twan-van-laarhoven, J. Tsivtsivadze, T. Urban, and . Heskes, Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics, IJCAR 2012, pp.378-392, 2012.
DOI : 10.1007/978-3-642-31365-3_30

J. Meng and L. C. Paulson, Lightweight relevance filtering for machine-generated resolution problems, Journal of Applied Logic, vol.7, issue.1, pp.41-57, 2009.
DOI : 10.1016/j.jal.2007.07.004

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher- Order Logic, LNCS, vol.2283, 2002.
DOI : 10.1007/3-540-45949-9

C. Lawrence and . Paulson, The inductive approach to verifying cryptographic protocols, J. Comput. Secur, vol.6, issue.12, pp.85-128, 1998.

C. Lawrence, J. C. Paulson, and . Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, EPiC, vol.2, pp.1-11, 2010.

C. Lawrence, K. Paulson, and . Susanto, Source-level proof reconstruction for interactive theorem proving, LNCS, vol.4732, pp.232-245, 2007.

A. Reynolds, C. Tinelli, and L. De-moura, Finding conflicting instances of quantified formulas in SMT, 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.195-202, 2014.
DOI : 10.1109/FMCAD.2014.6987613

S. Schulz, System Description: E??1.8, LNCS, vol.8312, pp.19-735, 2013.
DOI : 10.1007/978-3-642-45221-5_49

G. Sutcliffe, The 4th IJCAR automated theorem proving system competition?CASC-J4, pp.59-72, 2009.

G. Sutcliffe, The 6th IJCAR automated theorem proving system competition?CASC-J6, AI Commun, vol.26, issue.2, pp.211-223, 2013.

R. Thiemann and C. Sternagel, Certification of Termination Proofs Using CeTA, LNCS, vol.4, issue.2, pp.452-468, 2009.
DOI : 10.1007/978-3-540-25979-4_6

C. Urban and C. Kaliszyk, General bindings and alpha-equivalence in Nominal Isabelle, Log. Meth. Comput. Sci, vol.8, issue.214, pp.1-35, 2012.

J. Urban, MoMM ??? FAST INTERREDUCTION AND RETRIEVAL IN LARGE LIBRARIES OF FORMALIZED MATHEMATICS, International Journal on Artificial Intelligence Tools, vol.15, issue.01, pp.109-130, 2006.
DOI : 10.1142/S0218213006002588

J. Urban, MPTP 0.2: Design, Implementation, and Initial Experiments, Journal of Automated Reasoning, vol.15, issue.1, pp.21-43, 2006.
DOI : 10.1007/s10817-006-9032-3

J. Urban, MaLARea: A metasystem for automated reasoning in large theories, of CEUR Workshop Proceedings. CEUR-WS.org, 2007.

J. Urban, An overview of methods for large-theory automated theorem proving, ATE-2011 CEUR Workshop Proceedings, pp.3-8, 2011.

J. Urban, BliStr: The Blind Strategymaker, 2014.

J. Urban, P. Rudnicki, and G. Sutcliffe, ATP and Presentation Service for Mizar Formalizations, Journal of Automated Reasoning, vol.2, issue.2, pp.229-241, 2013.
DOI : 10.1007/s10817-012-9269-y

J. Urban, G. Sutcliffe, P. Pudlák, and J. Vysko?il, MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance, LNCS, vol.5195, pp.441-456, 2008.
DOI : 10.1007/978-3-540-71070-7_37

J. Urban and J. Vysko?il, Theorem Proving in Large Formal Mathematics as an Emerging AI Field, Automated Reasoning and Mathematics?Essays in Memory of William McCune, pp.240-257, 2013.
DOI : 10.1007/978-3-642-02959-2_10

A. Voronkov, AVATAR: The Architecture for First-Order Theorem Provers, CAV 2014, pp.696-710, 2014.
DOI : 10.1007/978-3-319-08867-9_46

M. Wenzel and . Isabelle, Isar?A generic framework for human-readable proof documents, From Insight to Proof?Festschrift in Honour of Andrzej Trybulec Studies in Logic, Grammar, and Rhetoric. Uniwersytet w Bia?ymstoku, 2007.