GFLean: An Autoformalisation Framework for Lean via GF

Vershinin, K., Paskevich, A.: Forthel—the language of formal theories. International Journal of Information Theories and Applications 7

2000

Earlier work this paper cites.

Zinn, C.: Understanding informal mathematical discourse. PhD thesis, Institut fur Informatik, Universitat Erlangen-Nurnberg (2004)

2004

Earlier work this paper cites.

Verchinine, K., Lyaletski, A., Paskevich, A.: System for automated deduction (sad): a tool for proof verification. In: International Conference on Automated Deduction. pp. 398–403. Springer (2007)

2007

Earlier work this paper cites.

Humayoun, M., Raffalli, C.: Mathnat-mathematical text in a controlled natural language. Special issue: Natural Language Processing and its Applications 46

2010

Earlier work this paper cites.

Kamp, H., Van Genabith, J., Reyle, U.: Discourse representation theory. In: Handbook of Philosophical Logic: Volume 15, pp. 125–394. Springer (2010)

2010

Earlier work this paper cites.

Ranta, A.: Grammatical framework: Programming with multilingual grammars, vol. 173. CSLI Publications, Center for the Study of Language and Information Stanford (2011)

2011

Earlier work this paper cites.

Ranta, A.: Translating between language and logic: what is easy and what is difficult. In: Automated Deduction–CADE-23: 23rd International Conference on Automated Deduction, Wrocław, Poland, July 31-August 5, 2011. Proceedings 23. pp. 5–25. Springer (2011)

2011

Earlier work this paper cites.

Ganesalingam, M.: The language of mathematics. Springer (2013)

2013

Earlier work this paper cites.

Chartrand, G., Polimeni, A.D., Zhang, P.: Mathematical proofs. chap. 3, pp. 81–104. Pearson (2017)

2017

Cited alongside, same era.

Wang, Q., Kaliszyk, C., Urban, J.: First experiments with neural translation of informal to formal mathematics. In: Intelligent Computer Mathematics: 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings 11. pp. 255–270. Springer (2018)

2018

Cited alongside, same era.

Buzzard, K., Commelin, J., Massot, P.: Formalising perfectoid spaces. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp. 299–312 (2020)

2020

Cited alongside, same era.

Ranta, A., Angelov, K., Gruzitis, N., Kolachina, P.: Abstract syntax as interlingua: Scaling up the grammatical framework from controlled languages to robust pipelines. Computational Linguistics 46

2020

Cited alongside, same era.

De Lon, A., Koepke, P., Lorenzen, A., Marti, A., Schütz, M., Wenzel, M.: The isabelle/naproche natural language proof assistant. In: Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28. pp. 614–624. Springer International Publishing (2021)

2021

Later among the works it cites.

Moura, L.d., Ullrich, S.: The lean 4 theorem prover and programming language. In: Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28. pp. 625–635. Springer (2021)

2021

Later among the works it cites.

Gadgil, S., Tadipatri, A.R., Agrawal, A., Narayanan, A., Goyal, N.: Towards automating formalisation of theorem statements using large language models. In: 36th Conference on Neural Information Processing Systems (NeurIPS 2022) Workshop on MATH-AI (2022)

2022

Later among the works it cites.

Wu, Y., Jiang, A.Q., Li, W., Rabe, M., Staats, C., Jamnik, M., Szegedy, C.: Autoformalization with large language models. Advances in Neural Information Processing Systems 35