Author name cluster

Andrej Bauer

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

2 author rows

NeurIPS Conference 2023 Conference Paper

MLFMF: Data Sets for Machine Learning for Mathematical Formalization

Andrej Bauer
Matej Petković
Ljupco Todorovski

We introduce MLFMF, a collection of data sets for benchmarking recommendation systems used to support formalization of mathematics with proof assistants. These systems help humans identify which previous entries (theorems, constructions, datatypes, and postulates) are relevant in proving a new theorem or carrying out a new construction. Each data set is derived from a library of formalized mathematics written in proof assistants Agda or Lean. The collection includes the largest Lean 4 library Mathlib, and some of the largest Agda libraries: the standard library, the library of univalent mathematics Agda-unimath, and the TypeTopology library. Each data set represents the corresponding library in two ways: as a heterogeneous network, and as a list of s-expressions representing the syntax trees of all the entries in the library. The network contains the (modular) structure of the library and the references between entries, while the s-expressions give complete and easily parsed information about every entry. We report baseline results using standard graph and word embeddings, tree ensembles, and instance-based learning algorithms. The MLFMF data sets provide solid benchmarking support for further investigation of the numerous machine learning approaches to formalized mathematics. The methodology used to extract the networks and the s-expressions readily applies to other libraries, and is applicable to other proof assistants. With more than $250\, 000$ entries in total, this is currently the largest collection of formalized mathematical knowledge in machine learnable format.

PDF Details

TCS Journal 2014 Journal Article

Cartesian closed categories of separable Scott domains

Andrej Bauer
Gordon D. Plotkin
Dana S. Scott

We classify all sub-cartesian closed categories of the category of separable Scott domains. The classification employs a notion of coherence degree determined by the possible inconsistency patterns of sets of finite elements of a domain. Using the classification, we determine all sub-cartesian closed categories of the category of separable Scott domains that contain a universal object. The separable Scott domain models of the λβ-calculus are then classified up to a retraction by their coherence degrees.

Details DOI

TCS Journal 2012 Journal Article

On the failure of fixed-point theorems for chain-complete lattices in the effective topos

Andrej Bauer

We show that in the effective topos there is a chain-complete distributive lattice with a monotone and progressive endomap which does not have a fixed point. An immediate consequence of this is that both Tarski’s theorem for chain-complete posets and the Bourbaki–Witt theorem have no constructive (topos-valid) proofs.

Details DOI

TCS Journal 2004 Journal Article

Equilogical spaces

Andrej Bauer
Lars Birkedal
Dana S. Scott

It is well known that one can build models of full higher-order dependent-type theory (also called the calculus of constructions) using partial equivalence relations (PERs) and assemblies over a partial combinatory algebra. But the idea of categories of PERs and ERs (total equivalence relations) can be applied to other structures as well. In particular, we can easily define the category of ERs and equivalence-preserving continuous mappings over the standard category Top 0 of topological T 0-spaces; we call these spaces (a topological space together with an ER) equilogical spaces and the resulting category Equ. We show that this category—in contradistinction to Top 0 —is a cartesian closed category. The direct proof outlined here uses the equivalence of the category Equ to the category PEqu of PERs over algebraic lattices (a full subcategory of Top 0 that is well known to be cartesian closed from domain theory). In another paper with Carboni and Rosolini (cited herein), a more abstract categorical generalization shows why many such categories are cartesian closed. The category Equ obviously contains Top 0 as a full subcategory, and it naturally contains many other well known subcategories. In particular, we show why, as a consequence of work of Ershov, Berger, and others, the Kleene–Kreisel hierarchy of countable functionals of finite types can be naturally constructed in Equ from the natural numbers object N by repeated use in Equ of exponentiation and binary products. We also develop for Equ notions of modest sets (a category equivalent to Equ) and assemblies to explain why a model of dependent type theory is obtained. We make some comparisons of this model to other, known models.

Details DOI

CSL Conference 2000 Conference Paper

Continuous Functionals of Dependent Types and Equilogical Spaces

Andrej Bauer
Lars Birkedal

Abstract We show that dependent sums and dependent products of continuous parametrizations on domains with dense, codense, and natural totalities agree with dependent sums and dependent products in equilogical spaces, and thus also in the realizability topos RT( $ RT\left( {\mathcal{P}\omega } \right) $ ).

Details