Fetching the paper…
Reading the bibliography…
We report on our experiments to train deep neural networks that automatically translate informalized LaTeX-written Mizar texts into the formal Mizar language.
Approximation by superpositions of a sigmoidal function
G. Cybenko · 1989
Earlier work this paper cites.
A collection of TeXed Mizar abstracts
A. Trybulec and P. Rudnicki · 1989
Earlier work this paper cites.
Approximation capabilities of multilayer feedforward networks
K. Hornik · 1991
Earlier work this paper cites.
Mizar and the machine translation of mathematics documents
G. Bancerek and P. Carlson · 1994
Earlier work this paper cites.
Bleu: a method for automatic evaluation of machine translation
K. Papineni, S. Roukos, T. Ward, and W. Zhu · 2002
Earlier work this paper cites.
Automatic translation in formalized mathematics
G. Bancerek · 2006
Earlier work this paper cites.
MPTP 0.2: Design, implementation, and initial experiments
J. Urban · 2006
Earlier work this paper cites.
Dense Sphere Packings: A Blueprint for Formal Proofs
T. Hales · 2012
Earlier work this paper cites.
ImageNet classification with deep convolutional neural networks
A. Krizhevsky, I. Sutskever, and G. E. Hinton · 2012
Cited alongside, same era.
Theorem proving in large formal mathematics as an emerging AI field
J. Urban and J. Vyskočil · 2013
Cited alongside, same era.
Learning phrase representations using rnn encoder–decoder for statistical machine translation
K. Cho, B. van Merriënboer, Ç. Gülçehre, D. Bahdanau, F. Bougares, H. Schwenk, and Y. Bengio · 2014
Cited alongside, same era.
Developing corpus-based translation methods between informal and formal mathematics: Project description
C. Kaliszyk, J. Urban, J. Vyskočil, and H. Geuvers · 2014
Cited alongside, same era.
Move evaluation in Go using deep convolutional neural networks
C. J. Maddison, A. Huang, I. Sutskever, and D. Silver · 2014
Cited alongside, same era.
Understanding LSTM networks
C. Olah · 2015
Later among the works it cites.
Hammering towards QED
J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban · 2016
Later among the works it cites.
Deep Learning
I. Goodfellow, Y. Bengio, and A. Courville · 2016
Later among the works it cites.
A formal proof of the Kepler conjecture
T. C. Hales, M. Adams, G. Bauer, D. T. Dang, J. Harrison, T. L. Hoang, C. Kaliszyk, V. Magron, S. McLaughlin, T. T. Nguyen, T. Q. Nguyen, T. Nipkow, S. Obua, J. Pleso, J. Rute, A. Solovyev, A. H. T. Ta, T. N. Tran, D. T. Trieu, J. Urban, K. K. Vu, and R. Zumkeller · 2017
Later among the works it cites.
Automating formalization by statistical and semantic parsing of mathematics
C. Kaliszyk, J. Urban, and J. Vyskočil · 2017
Later among the works it cites.
Neural machine translation (seq2seq) tutorial
M. Luong, E. Brevdo, and R. Zhao · 2017
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Sequence to sequence learning with neural networks
I. Sutskever, O. Vinyals, and Q. V. Le · 2014
Cited alongside, same era.
Mizar: State-of-the-art and beyond
G. Bancerek, C. Bylinski, A. Grabowski, A. Kornilowicz, R. Matuszewski, A. Naumowicz, K. Pak, and J. Urban · 2015
Cited alongside, same era.
Learning to parse on aligned corpora (rough diamond)
C. Kaliszyk, J. Urban, and J. Vyskočil · 2015
Cited alongside, same era.
G. Neubig · 2017
Later among the works it cites.