The tactic language is a special-purpose programming language for constructing proofs, indicated using the keyword by.
knownin1980s
knownin1980s is a term which provides a proof of an
arbitrary proposition. In this current phase of the FLT project,
knownin1980s will be allowed as a proof of any theorem
which would have been easy for an expert to deduce from
the pre-1990 literature. This stretches from standard easy
statements about things like elliptic curves to much deeper results
which are relatively short derivations from deep results published
pre-1990 such as Taylor's theorem attaching Galois representations
to Hilbert modular forms, Langlands' work on cyclic base change
and so on.
An invocation of knownin1980s should always be accompanied by comments
which indicate how one might prove this theorem using only results
which were in the mathematical literature before 1990. Note that it
does not have to be a precise reference to the literature; an argument
which is not explicitly in the literature but which is relatively
short and uses only techniques known in the 1980s is fine.
- Tags:
- Defined in module:
- FLT.Assumptions.KnownIn1980s