Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Mario Carneiro, Chad E. Brown, and Josef Urban. Automated Theorem Proving for Metamath. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{carneiro_et_al:LIPIcs.ITP.2023.9, author = {Carneiro, Mario and Brown, Chad E. and Urban, Josef}, title = {{Automated Theorem Proving for Metamath}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {9:1--9:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.9}, URN = {urn:nbn:de:0030-drops-183846}, doi = {10.4230/LIPIcs.ITP.2023.9}, annote = {Keywords: Metamath, Automated theorem proving, Interactive theorem proving, Formal proof assistants, proof discovery} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban. MizAR 60 for Mizar 50. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{jakubuv_et_al:LIPIcs.ITP.2023.19, author = {Jakub\r{u}v, Jan and Chvalovsk\'{y}, Karel and Goertzel, Zarathustra and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Mirek and Piotrowski, Bartosz and Schulz, Stephan and Suda, Martin and Urban, Josef}, title = {{MizAR 60 for Mizar 50}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {19:1--19:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.19}, URN = {urn:nbn:de:0030-drops-183942}, doi = {10.4230/LIPIcs.ITP.2023.19}, annote = {Keywords: Mizar, ENIGMA, Automated Reasoning, Machine Learning} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Oliver Nash. A Formalisation of Gallagher’s Ergodic Theorem. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{nash:LIPIcs.ITP.2023.23, author = {Nash, Oliver}, title = {{A Formalisation of Gallagher’s Ergodic Theorem}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {23:1--23:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.23}, URN = {urn:nbn:de:0030-drops-183981}, doi = {10.4230/LIPIcs.ITP.2023.23}, annote = {Keywords: Lean proof assistant, measure theory, metric number theory, ergodicity, Gallagher’s theorem, Duffin-Schaeffer conjecture} }
Published in: LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020)
Adam Bouland, Bill Fefferman, and Umesh Vazirani. Computational Pseudorandomness, the Wormhole Growth Paradox, and Constraints on the AdS/CFT Duality (Abstract). In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 63:1-63:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{bouland_et_al:LIPIcs.ITCS.2020.63, author = {Bouland, Adam and Fefferman, Bill and Vazirani, Umesh}, title = {{Computational Pseudorandomness, the Wormhole Growth Paradox, and Constraints on the AdS/CFT Duality}}, booktitle = {11th Innovations in Theoretical Computer Science Conference (ITCS 2020)}, pages = {63:1--63:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-134-4}, ISSN = {1868-8969}, year = {2020}, volume = {151}, editor = {Vidick, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.63}, URN = {urn:nbn:de:0030-drops-117486}, doi = {10.4230/LIPIcs.ITCS.2020.63}, annote = {Keywords: Quantum complexity theory, pseudorandomness, AdS/CFT correspondence} }
Published in: LIPIcs, Volume 99, 34th International Symposium on Computational Geometry (SoCG 2018)
Adam Brown and Bei Wang. Sheaf-Theoretic Stratification Learning. In 34th International Symposium on Computational Geometry (SoCG 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 99, pp. 14:1-14:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{brown_et_al:LIPIcs.SoCG.2018.14, author = {Brown, Adam and Wang, Bei}, title = {{Sheaf-Theoretic Stratification Learning}}, booktitle = {34th International Symposium on Computational Geometry (SoCG 2018)}, pages = {14:1--14:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-066-8}, ISSN = {1868-8969}, year = {2018}, volume = {99}, editor = {Speckmann, Bettina and T\'{o}th, Csaba D.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2018.14}, URN = {urn:nbn:de:0030-drops-87270}, doi = {10.4230/LIPIcs.SoCG.2018.14}, annote = {Keywords: Sheaf theory, stratification learning, topological data analysis, stratification} }
Feedback for Dagstuhl Publishing