# Beware of Words: Evaluating the Lexical Richness of Conversational Large
Language Models

Gonzalo Martínez<EMAIL_ADDRESS>,  José Alberto Hernández
<EMAIL_ADDRESS>Universidad Carlos III de MadridAvda de la Universidad
30LeganésMadridSpain28911 ,  Javier Conde<EMAIL_ADDRESS>,  Pedro
Reviriego<EMAIL_ADDRESS>Universidad Politécnica de MadridAvda
Complutense 30MadridMadridSpain28040 and  Elena Merino
<EMAIL_ADDRESS>Universidad de ValladolidPaseo del Cauce
59ValladolidValladolidSpain47011

(2023)

###### Abstract.

The performance of conversational Large Language Models (LLMs) in general, and
of ChatGPT in particular, is currently being evaluated on many different
tasks, from logical reasoning or maths to answering questions on a myriad of
topics. Instead, much less attention is being devoted to the study of the
linguistic features of the texts generated by these LLMs. This is surprising
since LLMs are models for language, and understanding how they use the
language is important. Indeed, conversational LLMs are poised to have a
significant impact on the evolution of languages as they may eventually
dominate the creation of new text. This means that for example, if
conversational LLMs do not use a word it may become less and less frequent and
eventually stop being used altogether. Therefore, evaluating the linguistic
features of the text they produce and how those depend on the model parameters
is the first step toward understanding the potential impact of conversational
LLMs on the evolution of languages. In this paper, we consider the evaluation
of the lexical richness of the text generated by LLMs and how it depends on
the model parameters. A methodology is presented and used to conduct a
comprehensive evaluation of lexical richness using ChatGPT as a case study.
The results show how lexical richness depends on the version of ChatGPT and
some of its parameters, such as the presence penalty, or on the role assigned
to the model. The dataset and tools used in our analysis are released under
open licenses with the goal of drawing the much-needed attention to the
evaluation of the linguistic features of LLM-generated text.

LLM, Lexical richness, ChatGPT, Evaluation

††copyright: acmlicensed††journalyear: 2023††doi: XXXXXXX.XXXXXXX††ccs:
Software and its engineering Empirical software validation††ccs: Computing
methodologies Natural language generation††ccs: Computing methodologies
Language resources

##  1\. Introduction

The introduction of ChatGPT in 2022 triggered an exponential adoption of Large
Language Model (LLM) based artificial intelligence tools. This has further
accelerated the development of LLMs which is now a top priority for
hyperscalers as shown by the recent introduction of Gemini (Team, 2023) by
Google or Grok111https://x.ai/model-card/ by xAI. These base LLMs are then
fine-tuned to obtain conversational LLMs, such as ChatGPT, that can answer
questions and follow instructions. As more and more LLM-based tools become
available, understanding their performance becomes critical; for example, to
select the right model for a given problem or to assess if a tool can be used
for that problem in the first place. Measuring the performance on different
tasks is also helpful in identifying limitations of the current models to
focus efforts for improvements in the next versions of the models or in newer
models developed from scratch.

The evaluation of conversational LLMs and more broadly of Artificial
Intelligence (AI) systems is challenging (Hernandez-Orallo, 2020). A large
number of benchmarks have been developed to evaluate the performance in a wide
range of tasks and topics. For example, extensive test suites to evaluate how
conversational LLMs solve mathematical problems are available (Hendrycks et
al., 2021b) covering different subjects in maths with thousands of problems.
Similarly, there are large benchmarks to evaluate conversational LLM knowledge
in many different areas with multiple-choice questions. For example (Hendrycks
et al., 2021a) includes 57 different tasks covering STEM, humanities, or
social sciences. The number of tasks is extended to more than 200 in (et al,
2023b). A similar approach is used in (Zellers et al., 2019) to test common
sense reasoning by choosing among different options to end a sentence. In
these benchmarks, the results are quantified with a percentage of correct
answers and models try to get as close as possible to 100%222See for example
Table 2 in (Team, 2023)..

Those elaborated benchmarks are capable of quantifying how conversational LLMs
perform on different tasks with good accuracy. However, conversational LLMs
are not only used to answer questions or to solve specific problems or games.
They will be increasingly used to generate text; soon novels or textbooks
written by conversational LLMs or with the help of LLMs will be common. Those
texts will be read by humans and possibly used as well to train new LLMs thus
influencing future writers both humans and LLMs (Martínez et al., 2023). In
the case of generative AI models like LLMs, the use of AI-generated data for
training can lead to performance issues (Bertrand et al., 2023; Briesch et
al., 2023). For humans, the texts they read condition language acquisition and
use. Therefore, it is of interest to understand how LLMs use the language. For
example, how do they use the vocabulary? If a word is not used by LLMs it will
become less and less frequent and may eventually fall in disuse. The lexical
richness333Range and variety of vocabulary used, equivalent to lexical
diversity (LD) as understood by McCarthy and Jarvis (McCarthy and Jarvis,
2007). of LLMs may thus have a significant impact on the evolution of the
lexicon of languages in the next decades.

These more subtle but fundamental questions are not adequately covered by
existing conversational LLM benchmarks and performance evaluation procedures.
Some works have considered the linguistic features of the text generated by
LLMs (Toro, 2023; Muñoz-Ortiz et al., 2023; Reviriego et al., 2023) analyzing
the presence of phonological biases and comparing some linguistic features or
the lexical richness of conversational LLMs and humans. However, to the best
of our knowledge, there has been no attempt to understand how the linguistic
features of conversational LLMs depend on the model parameters, the type of
text generated, or the context and role given to the LLM. Similarly, there is
no specific dataset that exercises conversational LLMs to produce different
types of texts that can be used to evaluate the linguistic features of LLMs.
In this paper we address both issues by 1) designing a simple dataset to
exercise text generation in conversational LLMs and 2) by using the dataset to
evaluate how lexical richness depends on the LLM parameters such as
temperature or top probability. The dataset and generated texts are publicly
available so that they can be used in the first case to conduct the same
evaluation for other conversational LLMs and in the second to enable other
researchers to perform linguistic analysis of the conversational LLM-generated
text.

The rest of the paper is organized as follows: section 2 identifies the
requirements to evaluate the lexical richness of LLMs, section 3 presents the
proposed methodology for the evaluation that includes both the selection of
prompts and parameters as well as the testing procedure. The results of the
evaluation of ChatGPT are presented in section 4 discussing the main findings.
The paper ends with the conclusions and a discussion of future work.

##  2\. Evaluating the Lexical Richness of Large Language Models

The lexical features of the text generated by the LLMs depend on multiple
factors. For example, on the task that the LLM is performing; the text to
answer a computing question can be very different from the one of a literary
essay. A similar reasoning applies to the role or context that is given to the
LLM, the text for the same task will be different if we ask the LLM to write
it as a child or as a sophisticated writer. Those two factors are similar to
what happens with humans, the text we produce depends on the task and person.
LLMs also have other configuration parameters that are directly related to the
model itself, for example, temperature or top probability. Therefore,
evaluating the lexical features or more broadly the linguistic features of
LLMs is a complex task that requires careful analysis to design a methodology
that can capture all those factors. To design such a methodology, it is also
important to understand what are the goals of the evaluation, which in our
case include:

  * •

Understanding the impact of the different factors (task, role, parameters) on
the lexical features of the generated text for a given model.

  * •

Comparing the lexical features of the text generated by different LLMs.

  * •

Comparing the lexical features of the text generated by LLMs and humans.

The first goal focuses on a single LLM and will enable us for example to
understand and quantify the lexical richness versus the temperature of the
model. As of today, we know that high-temperature values make the text more
creative and diverse, but how much? is the lexical richness task or role-
dependent? The second objective is of interest to compare the lexical features
as LLMs evolve, for example, how do the lexical features change from
ChatGPT3.5 (version gpt-3.5-turbo-1106) to ChatGPT4 (version
gpt4-1106-preview)? It is also of interest to compare the lexical features of
different LLMs, how different are the features of ChatGPT and Bard? Finally,
it is also interesting to see how different is the text generated by humans
and LLMs for the same task. Here, we are limited by the availability of human-
generated text. For LLMs, we can easily generate texts for different tasks,
roles, and parameter values. Unfortunately, for humans this is not the case,
there are only a few datasets of human-generated text for different tasks and
with limited information on the writers.

An evaluation of the lexical features of LLMs should ideally include:

  1. (1)

A large corpus of prompts for each task to ensure that the results are
representative of the text generated by the model.

  2. (2)

Different tasks and topics to test the model when writing different types of
text on different topics.

  3. (3)

Different roles to evaluate the importance of the role and context on the
generated text.

  4. (4)

Different hyperparameter configurations to assess the impact of each parameter
on the generated text.

In the next section, we propose an initial test suite to evaluate the lexical
richness of LLMs that tries to capture all those features focusing on the
evaluation of ChatGPT.

##  3\. Cave Verba: Beware of Words

In this section, we describe the methodology used to evaluate the lexical
richness of ChatGPT that we denote as “Cave Verba” a Latin expression coined
on the famous “cave canem”444Beware of the dog.. “Cave Verba” can be
translated as “beware of words”, which is intended to highlight the importance
of words in AI-generated texts but also to stress the carefulness needed when
studying its outputs. First, we describe the test suite, and then the testing
procedure. The test prompts, as well as the data generated, are shared555The
data for the TOEFL prompts is not shared as it is used for commercial
purposes. in a public repository666https://doi.org/10.5281/zenodo.10646082 so
that further linguistic analysis can be made on the text generated by ChatGPT
with different configurations and parameter values.

###  3.1. Test suite

The tests are intended to provide a comprehensive evaluation of the lexical
richness at a reasonable computational cost. In the following, tasks, roles,
and parameters used in the test are described.

####  3.1.1. Tasks and topics

The first part of the test suite is to define the tasks and associated
prompts. Since we are interested in the features of LLM-generated text we
focus on prompts that force the LLM to write new text and exclude
summarization or translation tasks. In particular, we consider the following
tasks:

  1. (1)

Essay writing: the LLM is asked to write a short essay about a given topic.

  2. (2)

Question answering: The LLM is asked to answer questions on different
topics777Note that the LLM is not given a choice of answers to select one as
in many existing benchmarks but rather asked to write a textual answer..

For essay writing two different sets of prompts are used. The first one
corresponds to TOEFL essays888https://github.com/rexshijaku/chatgpt-generated-
text-detection-corpus/blob/main/full_texts/questions.txt and the second to
topics compiled by the New York
Times999https://www.nytimes.com/2023/07/19/learning/175-writing-prompts-to-
spark-discussion-and-reflection.html for argumentative and narrative writing.
For question answering, we use data from the HC3
dataset101010https://huggingface.co/datasets/Hello-SimpleAI/HC3/. In
particular, subsets of 40 questions on medicine, finance, computing, open, and
Reddit are randomly selected from those categories in the HC3
dataset111111Several such subsets were tested for each category with a few
model settings to check that they produce similar lexical richness metrics..

A summary of the data used is given in Table 1. It can be seen that we have a
large number of prompts that are distributed on different tasks and topics and
come from different sources to ensure that results are representative. In
total, over 500 prompts which is a reasonable size when taking into account
that prompts have to be tested for many different parameter values.

Table 1. Tasks testing data Task | Category | Number of prompts
---|---|---
Essay writing | TOEFL | 126
Essay writing | NYT argumentative | 57
Essay writing | NYT narrative | 118
Question answering | open | 40
Question answering | finance | 40
Question answering | medicine | 40
Question answering | Reddit | 40
Question answering | computing | 40

####  3.1.2. Roles

To assess the impact of the role assigned to the LLM on lexical richness, we
have selected a set of roles that are expected to be different in terms of
their use of the language and, in particular, of its lexicon. The effect of
social parameters on language is studied by sociolinguistics (Wardhaugh and
Fuller, 2014). For example, social class, gender, age, educational level, or
ethnicity can influence the use of the language at different levels: phonetic,
morphological, syntactic, lexical-semantic, and textual (Labov, 1972). The
number of sociolinguistic investigations conducted in the field of written
production is much lower compared to those related to oral production (Lillis
and McKinney, 2013), and often, English is not used as the experimental
language. Nevertheless, we believe that their general findings can be
extrapolated for the purposes of an initial comparative analysis with the
results of AI production through role assignment by considering age, social
class, and gender.

Regarding social class, it is expected that speakers from higher classes
produce texts with a richer lexicon than those from lower classes (Shi and
Lei, 2021). In terms of age, adults have a more extensive vocabulary than
children (Johansson, 2008), and the effects of aging may influence lexical
impoverishment (Robert and Duarte, 2015; Gerstenberg, 2015). Differences in
linguistic production based on gender are the subject of recent research and
exhibit a highly heterogeneous nature, in (Singh, 2001) after analyzing the
oral production of a group of 17 women and 13 men, it was found that male
discourse was richer with generally longer sentences. In contrast, female
discourse contained shorter sentences with more lexical repetitions. In
broader spectrum studies, gender differences were found to be irrelevant
(Johansson, 2008). Other studies have found only slight gender differences in
linguistics features in formal and informal contexts, such as word length,
which is greater in male subjects, or the number of adjectives used, with a
higher usage observed in female groups (Koppen et al., 2017).

Based on these studies, we have selected eleven roles for evaluation:

  1. (1)

Default: No role is assigned to the LLM, the default role is used.

  2. (2)

Child: The LLM is requested to answer as a five-year-old child.

  3. (3)

Young adult male: The LLM is requested to answer as a young male adult.

  4. (4)

Young adult female: The LLM is requested to answer as a young female adult.

  5. (5)

Elderly adult male: The LLM is requested to answer as an elderly male adult.

  6. (6)

Elderly adult female: The LLM is requested to answer as an elderly female
adult.

  7. (7)

Affluent adult male: The LLM is requested to answer as an affluent male adult.

  8. (8)

Affluent adult female: The LLM is requested to answer as an affluent female
adult.

  9. (9)

Lower-class adult male: The LLM is requested to answer as a lower-class male
adult.

  10. (10)

Lower-class adult female: The LLM is requested to answer as a lower-class
female adult.

  11. (11)

Erudite121212The term erudite is used to try to make the LLM answer as a
highly educated native user of the language.: The LLM is requested to answer
as an erudite who uses a rich vocabulary.

These roles are intended to provide information on how age, gender, and social
class factors influence the lexical richness of AI-generated text.

####  3.1.3. LLM parameters

The hyperparameters of each LLM are different and thus the testing has to be
adjusted for each model. However, the differences are in many cases small and
some parameters are common to most LLMs. Therefore a similar approach can be
used for the testing. In our evaluation, we focus on OpenAI conversational
tools: the well-known ChatGPT which uses as base different LLMs, such as GPT4
(OpenAI, 2023). ChatGPT is a commercial product and not many details are
provided on how the base LLM is modified or complemented, additionally, the
API provides limited visibility into the model results and thus our evaluation
approach is to consider ChatGPT as a black box. The main model parameters that
are accessible through their API131313https://platform.openai.com/docs/api-
reference are described by OpenAI as follows:

  1. (1)

Temperature: “Higher values like 0.8 will make the output more random, while
lower values like 0.2 will make it more focused and deterministic.”

  2. (2)

Top probability: “An alternative to sampling with temperature, called nucleus
sampling, where the model considers the results of the tokens with top_p
probability mass. So 0.1 means only the tokens comprising the top 10%
probability mass are considered.”

  3. (3)

Frequency penalty: “Number between -2.0 and 2.0. Positive values penalize new
tokens based on their existing frequency in the text so far, decreasing the
model’s likelihood to repeat the same line verbatim.”

  4. (4)

Presence penalty: “Number between -2.0 and 2.0. Positive values penalize new
tokens based on whether they appear in the text so far, increasing the model’s
likelihood to talk about new topics.”

From their descriptions, it seems that all four parameters can affect the
lexical richness of the generated text and should be evaluated. The parameters
are also quite general and similar parameters are available in other LLMs like
Llama (et al, 2023c) or Mistral (et al, 2023a). Temperature is a classical
parameter to control how probabilities are assigned in the Softmax
normalization that maps values from the last layer of the model to the
probabilities of each token being selected (He et al., 2018). The top
probability or top_p is also a common parameter in LLMs and restricts the
choice to the tokens that concentrate most of the probability, so the sampling
is done from the most likely tokens only (Holtzman et al., 2020). The last two
parameters try to avoid repetitions in the text by introducing a penalty for
frequently used tokens or for all tokens that have been already used in the
generated text, similar parameters are common in other LLMs too. After
describing each of the parameters, it seems that all four are likely to have
an impact on the lexical richness of the generated text.

###  3.2. Test procedure

The first step in the evaluation is to generate the text with the AI model.
This is done with a script that makes calls to OpenAI’s models with the
desired parameter values and context and iterates over all the prompts in the
different tasks and topics to produce the result files with the text. Those
files are then processed, and the relevant lexical richness metrics are
computed.

The LexicalRichness module (Shen, 2022) is then used to compute the metrics
for each of the categories in each task. Four metrics are selected for the
comparisons. Two of them are based on the types and tokens over the entire set
of texts for the category, and two are computed for each of the texts
individually and then averaged to report the mean value. The first two metrics
are intended to capture the lexical richness over the entire set of answers
for each category. The other two metrics focus on measuring the lexical
richness of each of the answers and then take the average per category.

In more detail, the Root Type-Token Ratio (RTTR) and the Maas metric are
calculated on the texts of a given category (Hout and Vermeer, 2007; Tweedie
and Baayen, 1998). These metrics are based on the total number of words
($nTokens$) and the number of distinct words ($nTypes$) and introduce
modifications over the plain Type-Token Ratio (TTR) metric to make them
independent of the number of words in the text. In particular:

(1) $RTTR=\frac{nTypes}{\sqrt{nTokens}}$

(2) $Maas=\frac{\log(nTokens)-\log(nTypes)}{[\log(nTokens)]^{2}}$

For example, for the TOEFL category and default settings, the 126 essays
generated by ChatGPTv3.5 have in total 52,778 words and 4,551 distinct words
which are used as the token and types on the calculations of the RTTR and Maas
metrics, with values of 19.8 and 0.02 respectively. Therefore, with these two
metrics the richness of the lexicon used across all the TOEFL essays is
evaluated.

Additionally, two alternative metrics are computed for each of the texts: the
Moving average TTR (MATTR) (Covington and McFall, 2010) and the Measure of
Lexical Diversity (MTLD) (McCarthy and Jarvis, 2010). These metrics operate
sequentially on the text considering blocks or segments. For example, MTLD
counts words until the TTR reaches a predefined threshold and then starts a
new segment, and so on. For these metrics, since the answers are independent
merging them and computing the metric on the entire set can create artifacts.
Therefore, it is more appropriate to evaluate the metric for each of the texts
individually and then report the average across all the texts in a given
category. Therefore these metrics evaluate the lexical richness of each essay
individually and independently from the rest of the essays in the same
category indicating the lexical richness of each essay in isolation.

Finally, the trends and relative results are similar when the texts are
preprocessed to keep only the lemmas or when removing the most common stop
words. Therefore, the observed dependencies of lexical richness on the model’s
parameters and context seem to be independent of the lemmatization or
preprocessing done on the texts.

##  4\. Evaluation Results

As discussed before, our goal in these experiments is to understand the impact
of the model parameters on lexical richness. To that end, we have run the
entire dataset of prompts for ChatGPT3.5141414The exact models used in the
evaluation are ’gpt-3.5-turbo-1106’ and ’gpt-4-1106-preview’. For ChatGPT4, we
have selected the NYT dataset and run both argumentative and narrative
prompts.

The results are shown in the following figures which are divided into two
groups, one for the metrics that are computed per prompt (MATTR and MTLD) and
another for the metrics that are computed for all the prompts in each
category. In the first case, the metrics are computed per prompt and the
average for all prompts in each category is reported as discussed in the
previous section. The values used for each category are the following:

  1. (1)

Role: Default (D), child (C), young adult male (YAM), young adult female
(YAF), elderly adult male (EAM), elderly adult male (EAF), affluent adult male
(AAM), affluent adult female (AAF), lower class adult male (LAM), lower class
adult female (LAF) and erudite (ERU).

  2. (2)

Temperature: 0, 0.2, 0.4, 0.6, 0.8, 1,0, 1.2, 1.4, 1.6, 1.8, 2.0.

  3. (3)

Top_p: 0, 0.1, 0.2, 0.3, 0.4, 0.5, 0.6, 0.7, 0.8, 0.9, 1.

  4. (4)

Presence penalty: -2.0, -1.5, -1, -0.5, 0, 0.5, 1, 1,5, 2.0.

  5. (5)

Frequency penalty: -2.0, -1.5, -1, -0.5, 0, 0.5, 1, 1,5, 2.0.

The results for the first pair of metrics and the four model parameters are
summarized in figures 1,2,3,4. It can be seen that both MATTR and MTLD
increase significantly with temperature and frequency penalty. Looking at the
text generated for high values of both parameters (and for negative values of
the frequency penalty), it is often incorrect with non-valid words and
repetitions of letters and words. This occurs for both ChatGPT3.5 and
ChatGPT4. In more detail when the temperature is equal to or larger than 1.4
or when the frequency penalty is equal to or smaller than -0.5 or equal to or
larger than 1.0, the percentage of non-valid words is large so the text
generated is not useful. The range values for which incorrect texts are
generated are marked in red in the figures and not considered in the analysis.
For top probability and presence penalty, this effect was not observed and
texts were valid for all the values of these two parameters.

The effects of high temperature or frequency penalty values are illustrated
with two examples of excerpts from the model answers: “Humans are social
creatures, and we often seek thoughtful governance as appealing undertaking
lengthy fulfilievedg bent structure ballo Furthermore recovering distresso
well burAdditionallyilationrequested whenhigh.utilisation ret burden serieEdit
teal” or “In conclusion,itisdiretenely crucial renember
preservesavingaraelemtery environmental nhaturalresourcesinfrom morleywalmon
polutionseaLeverls.Designed implemented windows utility ultimate goal yayhd
ashes reasons psothosglobaleyare”. It is clear that those parameter values
should not be used.

Considering only the range of values that produce valid texts, the temperature
does not seem to affect MATTR and MTLD significantly, only a small increase is
observed when raising the temperature. Similarly, for the frequency penalty,
only two values (0 and 0.5) provide consistent and valid texts and the lexical
richness is slightly larger for the largest value (0.5). The top probability
does not seem to have any relevant impact on the lexical richness of the
generated text except for ChatGPT4 which shows a small increment when the top
probability is 1.0. Finally, the lexical richness shows an approximately
linear behavior with the presence penalty. The trends are consistent across
all the tasks and categories.

Looking at the lexical richness of ChatGPT3.5 and ChatGPT4, for the same
settings, ChatGPT4 has a larger richness in most cases. The richness is also
generally larger for essay writing (TOEFL and NYT) than for question answering
(HC3).

Figure 1. Lexical richness per prompt metrics (MATTR, MTLD) average across all
prompts versus Temperature, range values that produce incorrect results are
marked in red.

Figure 2. Lexical richness per prompt metrics (MATTR, MTLD) average across all
prompts versus Top Probability.

Figure 3. Lexical richness per prompt metrics (MATTR, MTLD) average across all
prompts versus Frequency Penalty, range values that produce incorrect results
are marked in red.

Figure 4. Lexical richness per prompt metrics (MATTR, MTLD) average across all
prompts versus Presence Penalty.

The results for the different roles on the first pair of metrics are shown in
Figure 5. It can be observed that lexical richness is lower for the “child”
role while for the rest differences are small. It seems that age (excluding
children), sex, or social class do not have a significant impact on the MATTR
or the MTLD metrics. Comparing ChatGPT4 versus ChatGPT3.5, richness tends to
be larger for essay writing than for question answering as in previous
results.

Figure 5. Lexical richness per prompt metrics (MATTR, MTLD) average across all
prompts for different roles.

The results for the second pair of metrics and the four parameters of the
model are summarized in figures 6,7,8,9. Note that in the case of the Maas
metric, more lexical richness corresponds to lower values. It can be seen that
in general, they are consistent with the other two metrics. The results for
temperature and frequency penalty show large differences in the regions where
the output text is often invalid and a small increase with the parameter value
in the rest of the range. The top probability does not have any significant
impact on the metrics, only a small increase for values close to 1.0. Finally,
the presence penalty increases the lexical richness with larger (smaller)
values of the RTTR (Maas) metrics. As for MATTR and MTLD, the trends are
consistent across all the tasks and categories considered and for both
ChatGPT3.5 and ChatGPT4. Comparing the lexical richness of ChatGPT3.5 and
ChatGPT4, for the same settings, ChatGPT4 has a larger richness in most cases
as for the other two metrics.

Figure 6. Lexical richness global metrics (Maas, RTTR) versus Temperature,
range values that produce incorrect results are marked in red.

Figure 7. Lexical richness global metrics (Maas, RTTR) versus Top Probability.

Figure 8. Lexical richness global metrics (Maas, RTTR) versus Frequency
Penalty, range values that produce incorrect results are marked in red.

Figure 9. Lexical richness global metrics (Maas, RTTR) versus Presence
Penalty.

The results for the different roles on the second pair of metrics are shown in
Figure 10. It can be observed that lexical richness is lower for the “child”
role as in the first two metrics. Additionally, it is also higher for
“erudite” which was not the case in MATTR and MTLD. For the rest of the roles,
differences are small and there is no clear trend. Therefore, age, sex, and
social class do not seem to have a significant impact on lexical richness.
This means that in terms of lexical richness, there seems to be no reason to
be concerned about gender bias in ChatGPT (Zhou and Sanfilippo, 2023). The
results for the child role may be due to the common use in the training of the
models of datasets like ELI5 (Explain Like I am 5 years old) in which the
questions ask for the answer to be written for a child (Fan et al., 2019).

Figure 10. Lexical richness global metrics (Maas, RTTR) for different roles.

The analysis of the results can be summarized in the following insights:

  1. (1)

ChatGPT4 produces texts with larger lexical richness than ChatGPT3.5.

  2. (2)

The temperature and frequency penalty parameters produce invalid texts for
some ranges of values that are excluded from the analysis.

  3. (3)

Temperature: lexical richness increases slightly with temperature.

  4. (4)

Frequency penalty: lexical richness increases slightly with frequency penalty.

  5. (5)

Presence penalty: lexical richness increases with the presence penalty.

  6. (6)

Top probability: has no effect on lexical richness unless for a small increase
for values close to 1.0.

  7. (7)

Role: Age, sex, or social class seem to have little impact on lexical richness
except when the age is that of a child.

  8. (8)

Role: asking the model explicitly to use a rich vocabulary (Erudite) increases
the global lexical richness metrics (RTTR and Mass) but not so much on the
local ones (MATTR and MTLD).

  9. (9)

Task: lexical richness is generally larger for essay writing (TOEFL, NYT) than
for question answering (HC3),

These insights provide users with criteria to select the values of the model
parameters to control the lexical richness of the generated text and also to
understand how parameter values selected for other reasons will impact lexical
richness. This illustrates the usefulness of carrying out the lexical richness
evaluation of LLMs. Finally, it is also important to note that our evaluation
has focused on ChatGPT when used to answer questions and write essays on
different topics. In other applications and uses, lexical richness may show
other dependencies with the model parameters.

##  5\. Conclusion

This work has evaluated the impact on the lexical richness of the text
generated by ChatGPT of the main model parameters such as temperature and top
probability and also of assigning different roles to the model. To that end, a
dataset has been created that exercises the models on different tasks and
topics. This dataset has then been used to evaluate ChatGPT3.5 and ChatGPT4.
The results show that lexical richness increases with the presence penalty.
This is reasonable as the presence penalty is a parameter that prevents the
model from using words that have already been used. The results for other
parameters that could be expected to also impact lexical richness such as the
frequency penalty or the temperature are limited as invalid texts are
generated over wide ranges of the possible values. The top probability that
restricts the model choices to the token with the highest scores does not seem
to have a significant impact on the lexical richness except for values close
to one. Considering the roles, assigning a role to the model does not seem to
affect its lexical richness in terms of sex, age, and social class except when
the model is asked to behave as a child. The results when the model is asked
to behave as an erudite are mixed, it increases the lexical richness according
to two of the metrics and it does not for the other two metrics. Finally,
lexical richness tends to be larger for essay writing than for question
answering.

The dataset and evaluation methodology presented in this paper is intended to
facilitate further research on the lexical richness of LLMs. The prompts used
as well as the texts generated are available in a public repository so that
they can be used to analyze other linguistic features. Future work can explore
the lexical richness of other LLMs. This would enable a better understanding
of the impact of the model parameters on lexical richness and also a
comparison of different LLMs in terms of their use of the lexicon.

###### Acknowledgements.

This work was supported by the FUN4DATE (PID2022-136684OB-C21/C22) project
funded by the Spanish Agencia Estatal de Investigacion (AEI)
10.13039/501100011033 and by the OpenAI research access program.

## References

  * (1)
  * Bertrand et al. (2023) Quentin Bertrand, Avishek Joey Bose, Alexandre Duplessis, Marco Jiralerspong, and Gauthier Gidel. 2023.  On the Stability of Iterative Retraining of Generative Models on their own Data.  arXiv:2310.00429 [cs.LG]
  * Briesch et al. (2023) Martin Briesch, Dominik Sobania, and Franz Rothlauf. 2023.  Large Language Models Suffer From Their Own Output: An Analysis of the Self-Consuming Training Loop.  arXiv:2311.16822 [cs.LG]
  * Covington and McFall (2010) Michael A. Covington and Joe D. McFall. 2010.  Cutting the Gordian Knot: The Moving-Average Type–Token Ratio (MATTR).  _Journal of Quantitative Linguistics_ 17, 2 (2010), 94–100.  https://doi.org/10.1080/09296171003643098 arXiv:https://doi.org/10.1080/09296171003643098
  * et al (2023a) Albert Q. Jiang et al. 2023a.  Mistral 7B.  arXiv:2310.06825 [cs.CL]
  * et al (2023b) Aarohi Srivastava et al. 2023b.  Beyond the Imitation Game: Quantifying and extrapolating the capabilities of language models.  arXiv:2206.04615 [cs.CL]
  * et al (2023c) Hugo Touvron et al. 2023c.  Llama 2: Open Foundation and Fine-Tuned Chat Models.  arXiv:2307.09288 [cs.CL]
  * Fan et al. (2019) Angela Fan, Yacine Jernite, Ethan Perez, David Grangier, Jason Weston, and Michael Auli. 2019.  ELI5: Long form question answering.  _arXiv preprint arXiv:1907.09190_ (2019).
  * Gerstenberg (2015) Annette Gerstenberg. 2015.  _A Sociolinguistic Perspective on Vocabulary Richness in a seven-year Comparison of Older Adults_.  109–127.  https://doi.org/10.1075/impact.37.06ger
  * He et al. (2018) Yu-Lin He, Xiao-Liang Zhang, Wei Ao, and Joshua Zhexue Huang. 2018.  Determining the optimal temperature parameter for Softmax function in reinforcement learning.  _Applied Soft Computing_ 70 (2018), 80–85.  https://doi.org/10.1016/j.asoc.2018.05.012
  * Hendrycks et al. (2021a) Dan Hendrycks, Collin Burns, Steven Basart, Andy Zou, Mantas Mazeika, Dawn Song, and Jacob Steinhardt. 2021a.  Measuring Massive Multitask Language Understanding. In _International Conference on Learning Representations_.  https://openreview.net/forum?id=d7KBjmI3GmQ
  * Hendrycks et al. (2021b) Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021b.  Measuring Mathematical Problem Solving With the MATH Dataset.  arXiv:2103.03874 [cs.LG]
  * Hernandez-Orallo (2020) Jose Hernandez-Orallo. 2020.  AI evaluation: On broken yardsticks and measurement scales. In _Workshop on Evaluating Evaluation of Ai Systems at AAAI_.
  * Holtzman et al. (2020) Ari Holtzman, Jan Buys, Li Du, Maxwell Forbes, and Yejin Choi. 2020.  The Curious Case of Neural Text Degeneration.  arXiv:1904.09751 [cs.CL]
  * Hout and Vermeer (2007) Roeland Hout and Anne Vermeer. 2007.  Comparing measures of lexical richness.  _In: H. Daller, J. Milton and J. Treffers-Daller (eds.), Modelling and assessing vocabulary knowledge (93-116). Cambridge: Cambridge University Press._ (01 2007).
  * Johansson (2008) Victoria Johansson. 2008.  _Lexical diversity and lexical density in speech and writing_.  WorkingPaper.  The information about affiliations in this record was updated in December 2015. The record was previously connected to the following departments: Linguistics and Phonetics (015010003).
  * Koppen et al. (2017) Kim Koppen, Mirjam Ernestus, and Margot van mulken. 2017.  The influence of social distance on speech behavior: Formality variation in casual speech.  _Corpus Linguistics and Linguistic Theory_ 15 (01 2017).  https://doi.org/10.1515/cllt-2016-0056
  * Labov (1972) W. Labov. 1972.  _Sociolinguistic Patterns_.  University of Pennsylvania Press.
  * Lillis and McKinney (2013) Theresa Lillis and Carolyn McKinney. 2013.  The sociolinguistics of writing in a global context: Objects, lenses, consequences.  _Journal of Sociolinguistics_ 17, 4 (2013), 415–439.  https://doi.org/10.1111/josl.12046 arXiv:https://onlinelibrary.wiley.com/doi/pdf/10.1111/josl.12046
  * Martínez et al. (2023) Gonzalo Martínez, Lauren Watson, Pedro Reviriego, José Alberto Hernández, Marc Juarez, and Rik Sarkar. 2023.  Towards Understanding the Interplay of Generative Artificial Intelligence and the Internet.  arXiv:2306.06130 [cs.AI]
  * McCarthy and Jarvis (2007) Philip M. McCarthy and Scott Jarvis. 2007.  vocd: A theoretical and empirical evaluation.  _Language Testing_ 24, 4 (2007), 459–488.  https://doi.org/10.1177/0265532207080767 arXiv:https://doi.org/10.1177/0265532207080767
  * McCarthy and Jarvis (2010) Philip M. McCarthy and Scott Jarvis. 2010.  MTLD, vocd-D, and HD-D: A validation study of sophisticated approaches to lexical diversity assessment.  _Behavior Research Methods_ 42 (2010), 381–392.
  * Muñoz-Ortiz et al. (2023) Alberto Muñoz-Ortiz, Carlos Gómez-Rodríguez, and David Vilares. 2023.  Contrasting Linguistic Patterns in Human and LLM-Generated Text.  _arXiv preprint arXiv:2308.09067_ (2023).
  * OpenAI (2023) OpenAI. 2023.  GPT-4 Technical Report.  arXiv:2303.08774 [cs.CL]
  * Reviriego et al. (2023) Pedro Reviriego, Javier Conde, Elena Merino-Gómez, Gonzalo Martínez, and José Alberto Hernández. 2023.  Playing with Words: Comparing the Vocabulary and Lexical Richness of ChatGPT and Humans.  arXiv:2308.07462 [cs.CL]
  * Robert and Duarte (2015) Christelle Robert and Liliana Rico Duarte. 2015.  Semantic Richness and Aging: The Effect of Number of Features in the Lexical Decision Task.  _Journal of Psycholinguistic Research_ 45 (2015), 359 – 365.
  * Shen (2022) Lucas Shen. 2022.  LexicalRichness: A small module to compute textual lexical richness.  https://doi.org/10.5281/zenodo.6607007
  * Shi and Lei (2021) Yaqian Shi and Lei Lei. 2021.  Lexical use and social class: A study on lexical richness, word length, and word class in spoken English.  _Lingua_ 262 (2021), 103155.  https://doi.org/10.1016/j.lingua.2021.103155
  * Singh (2001) Sameer Singh. 2001.  A Pilot Study on Gender Differences in Conversational Speech on Lexical Richness Measures.  _Literary and Linguistic Computing_ 16, 3 (09 2001), 251–264.  https://doi.org/10.1093/llc/16.3.251 arXiv:https://academic.oup.com/dsh/article-pdf/16/3/251/10889545/251.pdf
  * Team (2023) Gemini Team. 2023.  Gemini: A Family of Highly Capable Multimodal Models.  arXiv:2312.11805 [cs.CL]
  * Toro (2023) Juan Manuel Toro. 2023.  Emergence of a phonological bias in ChatGPT.  _arXiv preprint arXiv:2305.15929_ (2023).
  * Tweedie and Baayen (1998) Fiona J Tweedie and R Harald Baayen. 1998.  How variable may a constant be? Measures of lexical richness in perspective.  _Computers and the Humanities_ 32 (1998), 323–352.
  * Wardhaugh and Fuller (2014) Ronald Wardhaugh and Janet Fuller. 2014.  _An Introduction to Sociolinguistics_ (7 ed.).  Wiley.
  * Zellers et al. (2019) Rowan Zellers, Ari Holtzman, Yonatan Bisk, Ali Farhadi, and Yejin Choi. 2019.  HellaSwag: Can a Machine Really Finish Your Sentence?. In _Annual Meeting of the Association for Computational Linguistics_.
  * Zhou and Sanfilippo (2023) Kyrie Zhixuan Zhou and Madelyn Rose Sanfilippo. 2023.  Public perceptions of gender bias in large language models: Cases of chatgpt and ernie.  _arXiv preprint arXiv:2309.09120_ (2023).


This theorem does not exist as a lemma in mathlib, however, it might exist as
an instance. This is not a case of contamination, since the proofs are very
different - the one in mathlib is dependent on properties of emetric\_space,
while our proof is an explicit construction.

We also gave the correct Lean statement to Codex and evaluated its proof
output. Overall the performance was worse than before. Codex exchanged norm
with absolute value, and had a shorter outline than before.

_Theorem statement:_

$\mathbb{R}^{n}$ is paracompact for all $n$.

_Natural language proof:_

Let $\mathcal{A}$ be an open covering of $\mathbb{R}^{n}$.

We now construct a locally finite open refinement $\mathcal{C}$ of
$\mathcal{A}$ that covers $\mathbb{R}^{n}$. First, we define a collection of
pen balls. Let $B_{0}=\phi$, and for each $n\in\mathbb{N}$, let $B_{m}$ denote
the ball of radius $m$ centered at 0.

Given $m$, set $\bar{B_{m}}$ is compact in $\mathbb{R}^{n}$ by the Heine-Borel
theorem, so choose finitely many elements of $\mathcal{A}$ that cover
$\bar{B_{m}}$ and intersect each one with the open set
$\mathbb{R}^{n}\setminus\bar{B_{m-1}}$, and let $\mathcal{C}_{m}$ denote this
collection of open sets (each an open subset of an element of $\mathcal{A}$).
So $\mathcal{C}=\bigcup_{m=0}^{\infty}\mathcal{C}_{m}$ is an open refinement
of $\mathcal{A}$.

Note that $\mathcal{C}$ covers $\mathbb{R}^{n}$ since for any
$x\in\mathbb{R}^{n}$, there is a smallest $m\in\mathbb{N}$ such that
$x\in\bar{B_{m}}$ (namely, some $m$ where $\rVert x\lVert\leq m\leq\rVert
x\lVert+1$), and so $x$ is an element of $\mathcal{C}_{m}$.

Now collection $\mathcal{C}$ is locally finite since for given
$x\in\mathbb{R}^{n}$, neighborhood $B_{m}$ intersects only finitely many
elements of $\mathcal{C}$, namely those elements in collection
$\mathcal{C}_{1}\cup\mathcal{C}_{2}\cup\cdots\mathcal{C}_{m}$. So
$\mathcal{C}$ is a locally finite open refinement of $\mathcal{A}$ that covers
$\mathbb{R}^{n}$, hence $\mathbb{R}^{n}$ is paracompact.

$Q.E.D.$

_Codex Output_ The following is the best scored proof :

⬇

theorem rn_paracompact {n : ℕ} : paracompact (ℝ^n) :=

begin

– Let $\mathcal{A}$ be an open covering of $\mathbb{R}^n$.

assume A : set (set (ℝ^n)),

assume hA : is_open_cover A,

– We now construct a locally finite open refinement $\mathcal{C}$ of
$\mathcal{A}$ that covers $\mathbb{R}^n$.

– First, we define a collection of pen balls.

– Let $B_0 = \phi$, and for each $n \in \mathbb{N}$, let $B_m$ denote the ball
of radius $m$ centered at 0\.

let B : ℕ → set (ℝ^n) := λ m, ball 0 m,

let B0 : set (ℝ^n) := ∅,

have hB0 : B 0 = ∅, from rfl,

have hB : ∀ m : ℕ, B m = ball 0 m, from by {assume m : ℕ, rfl},

– Given $m$, set $\Bar{B_m}$ is compact in $\mathbb{R}^n$ by the Heine-Borel
theorem,

have hBm : ∀ m : ℕ, is_compact (closure (B m)), from by {

assume m : ℕ,

rw hB,

apply is_compact_closure,

apply is_compact_ball,

},

– so choose finitely many elements of $\mathcal{A}$ that cover $\Bar{B_m}$ and
intersect each one with the open set $\mathbb{R}^n \setminus \Bar{B_{m - 1}}$,

have h1 : ∀ m : ℕ, ∃ Cm : set (set (ℝ^n)), finite Cm ∧ ($\cup$₀ Cm) = (closure
(B m)) ∩ (set.compl (closure (B (m - 1)))), from by {

assume m : ℕ,

have h2 : ∃ Cm : set (set (ℝ^n)), finite Cm ∧ ($\cup$₀ Cm) = closure (B m),
from by {

rw hB,

apply hA,

apply hBm,

},

have h3 : ∃ Cm : set (set (ℝ^n)), finite Cm ∧ ($\cup$₀ Cm) = set.compl
(closure (B (m - 1))), from by {

have h4 : ∀ Bm : set (ℝ^n), is_open (set.compl Bm), from by {

assume Bm : set (ℝ^n),

apply is_open_compl,

apply is_open_closure,

apply is_open_ball,

},

rw hB,

apply hA,

apply h4,

},

use Cm ∩ (set.compl (closure (B (m - 1)))),

split,

apply finite.inter,

apply h2.left,

apply h3.left,

rw set.inter_compl_self,

rw h2.right,

rw h3.right,

rw set.compl_compl,

rw hB,

rw set.compl_compl,

rw hB0,

rw set.inter_empty,

rw set.union_empty,

},

– and let $\mathcal{C}_{m}$ denote this collection of open sets (each an open
subset of an element of $\mathcal{A}$).

let C : ℕ → set (set (ℝ^n)) := λ m, classical.some (h1 m).exists,

have hC : ∀ m : ℕ, C m = classical.some (h1 m).exists, from by {assume m : ℕ,
rfl},

have hCm : ∀ m : ℕ, finite (C m), from by {

assume m : ℕ,

rw hC,

apply (classical.some_spec (h1 m).exists).left,

},

have hCm2 : ∀ m : ℕ, ($\cup$₀ (C m)) = (closure (B m)) ∩ (set.compl (closure
(B (m - 1)))), from by {

assume m : ℕ,

rw hC,

apply (classical.some_spec (h1 m).exists).right,

},

– So $\mathcal{C} = \bigcup_{m = 0}^{\infty} \mathcal{C}_m$ is an open
refinement of $\mathcal{A}$.

let C_union : set (set (ℝ^n)) := $\cup$₀ (C ” (range (nat.succ))),

have hC_union : C_union = $\cup$₀ (C ” (range (nat.succ))), from rfl,

have hC_union2 : ∀ m : ℕ, C m ∈ C_union, from by {

assume m : ℕ,

rw hC_union,

apply set.mem_bUnion_iff,

use m,

split,

apply nat.mem_range,

rw hC,

rw set.mem_image_of_mem,

rw nat.succ_eq_add_one,

rw nat.add_comm,

},

have hC_union3 : ∀ m : ℕ, ∀ c ∈ C m, ∃ A ∈ A, c ⊆ A, from by {

assume m : ℕ,

assume c : set (ℝ^n),

assume hc : c ∈ C m,

rw hC,

rw set.mem_bUnion_iff at hc,

rcases hc with ⟨m,hm,hc⟩,

rw set.mem_image_of_mem at hc,

rcases hc with ⟨A,hm2,hc⟩,

use A,

split,

rw hm2,

apply hA,

rw hc,

apply set.inter_subset_left,

},

have hC_union4 : ∀ c ∈ C_union, ∃ A ∈ A, c ⊆ A, from by {

assume c : set (ℝ^n),

assume hc : c ∈ C_union,

rw hC_union at hc,

rw set.mem_bUnion_iff at hc,

rcases hc with ⟨m,hm,hc⟩,

rw set.mem_image_of_mem at hc,

rcases hc with ⟨cm,hm2,hc⟩,

rw hC at hc,

rw set.mem_bUnion_iff at hc,

rcases hc with ⟨m2,hm3,hc⟩,

rw hm2 at hm3,

have hm4 : m = m2, from nat.eq_of_succ_eq_succ hm3,

rw hm4 at hc,

rw set.mem_image_of_mem at hc,

rcases hc with ⟨A,hm5,hc⟩,

use A,

split,

rw hm5,

apply hA,

rw hc,

apply set.inter_subset_left,

},

have hC_union5 : is_open_refinement C_union A, from by {

apply is_open_refinement.intro,

apply hC_union4,

apply hC_union3,

},

– Note that $\mathcal{C}$ covers $\mathbb{R}^n$ since for any $x \in
\mathbb{R}^

end –Needs more than 2000 tokens

####  D.4.7 Symmetric real matrices have real eigenvalues

The formalisation of the statements scored 1 and 0 on average. Proof outlines
and proof with premises did the best. Codex could deduce that the eigenvalues
must be complex-valued, to begin with. It could also deduce the definitions of
symmetric matrices and eigenvalues. However, it had trouble formalising the
statement in mathlib style, probably since eigenvalues are defined in more
generality for endomorphisms, instead of matrices. There were also some
hallucinations.

The proof is mostly calculation based. Codex created a good outline, and could
deduce the correct meaning of $\bar{v}$ (complex conjugate). Sometimes there
were repetitions and irrelevant statements. For example, statements such as
have h1 : v = 0 and have h2 : v $\neq$ 0 appear consecutively at times. Codex
was also unable to ascribe the correct type to expressions of different kinds
appearing in the same statement : for $a\in\mathbb{R}$ and $b\in\mathbb{C}$,
Codex would output either a * b (incorrect) or a . b (correct but would
require additional changes further) instead of (a : $\mathbb{C}$) * b.

This theorem is uncontaminated as far as we know - the theorem statement might
exist in mathlib in a different and generalized manner, however, the
particular statement and proof given to Codex does not exist in mathlib.

_Theorem statement:_

Every real symmetric matrix has real eigenvalues.

_Natural language proof:_

Recall that if $z=a+bi$ is a complex number, its complex conjugate is defined
by $\bar{z}=a-bi$. We have $z\bar{z}=(a+bi)(a-bi)=a^{2}+b^{2}$, so $z\bar{z}$
is always a nonnegative real number (and equals 0 only when $z=0$ ). It is
also true that if $w,z$ are complex numbers, then
$\overline{wz}=\bar{w}\bar{z}$.

With this in mind, suppose that $\lambda$ is a (possibly complex) eigenvalue
of the real symmetric matrix $A$. Thus there is a nonzero vector $\mathbf{v}$,
also with complex entries, such that $A\mathbf{v}=\lambda\mathbf{v}$. By
taking the complex conjugate of both sides, and noting that $\bar{A}=A$ since
$A$ has real entries, we get
$\overline{A\mathbf{v}}=\overline{\lambda\mathbf{v}}\Rightarrow
A\overline{\mathbf{v}}=\bar{\lambda}\overline{\mathbf{v}}$. Then, using that
$A^{T}=A$,

$\displaystyle\overline{\mathbf{v}}^{T}A\mathbf{v}=\overline{\mathbf{v}}^{T}(A\mathbf{v})=\overline{\mathbf{v}}^{T}(\lambda\mathbf{v})=\lambda(\overline{\mathbf{v}}\cdot\mathbf{v})$
$\displaystyle\overline{\mathbf{v}}^{T}A\mathbf{v}=(A\overline{\mathbf{v}})^{T}\mathbf{v}=(\bar{\lambda}\overline{\mathbf{v}})^{T}\mathbf{v}=\bar{\lambda}(\overline{\mathbf{v}}\cdot\mathbf{v}).$

Since $\mathbf{v}\neq\mathbf{0}$, we have
$\overline{\mathbf{v}}\cdot\mathbf{v}\neq 0$. Thus $\lambda=\bar{\lambda}$,
which means $\lambda\in\mathbf{R}$

$Q.E.D$

_Codex Output_

Following is one of the best scored outputs (proof with premises, temperature
0.4) :

_Codex Output_

⬇

theorem real_symmetric_matrices_have_real_eigenvalues :

∀ A : matrix ℝ n n, symmetric A → ∀ λ : ℂ, is_eigenvalue A λ → is_real λ :=

begin

– Suppose that $\lambda$ is a (possibly complex) eigenvalue of the real
symmetric matrix $A$.

assume (A : matrix ℝ n n) (hA : symmetric A) (λ : ℂ) (hλ : is_eigenvalue A λ),

– Thus there is a nonzero vector $\mathbf{v}$, also with complex entries, such
that $A \mathbf{v}=\lambda \mathbf{v}$.

have h1 : ∃ (v : matrix ℂ n 1), v ≠ 0 ∧ A * v = λ • v, from by auto [hλ],

– By taking the complex conjugate of both sides, and noting that $\bar{A}=A$
since $A$ has real entries, we get $\overline{A \mathbf{v}}=\overline{\lambda
\mathbf{v}} \Rightarrow A \overline{\mathbf{v}}=\bar{\lambda}
\overline{\mathbf{v}}$.

have h2 : ∀ (v : matrix ℂ n 1), v ≠ 0 → A * v = λ • v → A * (v.conj) = λ.conj
• (v.conj), from

begin

– Suppose that $v$ is a nonzero vector with complex entries, and $A
\mathbf{v}=\lambda \mathbf{v}$.

assume (v : matrix ℂ n 1) (hv : v ≠ 0) (h3 : A * v = λ • v),

– By taking the complex conjugate of both sides, and noting that $\bar{A}=A$
since $A$ has real entries, we get $\overline{A \mathbf{v}}=\overline{\lambda
\mathbf{v}} \Rightarrow A \overline{\mathbf{v}}=\bar{\lambda}
\overline{\mathbf{v}}$.

have h4 : A * v.conj = λ.conj • v.conj, from

begin

– $\overline{A \mathbf{v}}=\overline{\lambda \mathbf{v}} \Rightarrow A
\overline{\mathbf{v}}=\bar{\lambda} \overline{\mathbf{v}}$.

have h5 : A * v.conj = λ.conj • v.conj, from by auto [hA, h3, conj_mul_conj,
conj_eq_of_eq_conj, mul_comm],

show A * v.conj = λ.conj • v.conj, from h5,

end,

show A * (v.conj) = λ.conj • (v.conj), from h4,

end,

– Then, using that $A^{T}=A$,

have h5 : ∀ (v : matrix ℂ n 1), v ≠ 0 → A * v = λ • v → λ = λ.conj, from

begin

– Suppose that $v$ is a nonzero vector with complex entries, and $A
\mathbf{v}=\lambda \mathbf{v}$.

assume (v : matrix ℂ n 1) (hv : v ≠ 0) (h6 : A * v = λ • v),

– Then, using that $A^{T}=A$,

have h7 : λ = λ.conj, from

begin

– $A^{T}=A$

have h8 : A.transpose = A, from by auto [hA, symmetric_transpose_eq],

– $A^{T}=A$

have h9 : A.transpose = A, from by auto [hA, symmetric_transpose_eq],

– $\overline{\mathbf{v}}^{T} A \mathbf{v}=\overline{\mathbf{v}}^{T}(A
\mathbf{v})=\overline{\mathbf{v}}^{T}(\lambda
\mathbf{v})=\lambda(\overline{\mathbf{v}} \cdot \mathbf{v})$

have h10 : (v.conj).transpose * A * v = λ * (v.conj).transpose * v, from by
auto [h6, mul_assoc, mul_comm],

– $\overline{\mathbf{v}}^{T} A \mathbf{v}=(A \overline{\mathbf{v}})^{T}
\mathbf{v}=(\bar{\lambda} \overline{\mathbf{v}})^{T}
\mathbf{v}=\bar{\lambda}(\overline{\mathbf{v}} \cdot \mathbf{v})$

have h11 : (v.conj).transpose * A * v = (λ.conj * v.conj).transpose * v, from
by auto [h9, h2, hv, h6, mul_assoc],

– Since $\mathbf{v} \neq \mathbf{0}$, we have $\overline{\mathbf{v}} \cdot
\mathbf{v} \neq 0$. Thus $\lambda=\bar{\lambda}$, which means $\lambda \in
\mathbf{R}$

have h12 : λ = λ.conj, from by auto [hv, h10, h11, mul_left_inj],

show λ = λ.conj, from h12,

end,

show λ = λ.conj, from h7,

end,

– Thus $\lambda \in \mathbf{R}$

show is_real λ, from by auto [h1, h5],

end

####  D.4.8 Class number of a PID

The formalisation of the statement got an average score of 1 or 0. Proof with
premises performed the best. The statement was relatively easy to formalise.
The only problem occuring sometimes was that Codex could not identify that PID
stands for principal ideal domain.

The proof is relatively short and majorly based on unfolding of definitions.
Codex deduced that the statement has an if and only if implementation and
hence split it. It got the outline of the proof right frequently, which could
easily be completed to a full proof.

While this theorem is present in mathlib, the NL proof provided to Codex was
very different from the proof in mathlib, and is minimally contaminated.

_Theorem statement:_

The class number of a number field $K$ is 1 if and only if the ring of
integers is a PID.

_Natural language proof:_

Let $R$ be the ring of integers corresponding to $K$. If $R$ is a PID, then,
by definition, the class group is trivial, hence it has class number $1.$

Conversely, if $R$ has class number 1 ,all ideals of $R$ are principal, hence
$R$ is a PID .

$Q.E.D$

_Codex Output_

Following is the best scored output (proof with premises, temperature 0.8) :

Codex Output

⬇

theorem class_number_one_iff_pid {K : Type*} [discrete_field K] :

class_number K = 1 ↔ is_pid (ring_of_integers K) :=

begin

– Let $R$ be the ring of integers corresponding to $K$.

assume hR : ring_of_integers K,

– If $R$ is a PID, then, by definition, the

– class group is trivial, hence it has class number $1 .$

have h1 : is_pid hR,

{

show is_pid hR, from by auto [is_pid],

},

have h2 : class_number K = 1,

{

show class_number K = 1, from by auto [class_number_of_pid],

},

show class_number K = 1 ↔ is_pid (ring_of_integers K), from by auto [h1, h2],

– Conversely, if $R$ has class number 1 ,

– all ideals of $R$ are principal, hence $R$ is a PID .$

have h3 : class_number K = 1,

{

show class_number K = 1, from by auto [class_number],

},

have h4 : is_principal_ideal hR,

{

show is_principal_ideal hR, from by auto [class_number_principal_ideals],

},

have h5 : is_pid hR,

{

show is_pid hR, from by auto [is_pid],

},

show class_number K = 1 ↔ is_pid (ring_of_integers K), from by auto [h3, h5],

end

####  D.4.9 Evaluation of Bernoulli polynomials

For this lemma, Codex was given the correct statement, and had to work out the
proof. However, it did not perform very well. While it demonstrates an
understanding of types, it seems to have a problem with translating the LateX
formulae for $n\choose k$. We also noticed that it applied strong induction,
as was needed, but sometimes faltered. The proof also had a bit of a backward
style element, which it easily managed to convert into forward style. On
average, it scored 1, with better scores at temperature 0.8.

This theorem is not present in mathlib, and is uncontaminated.

_Theorem statement:_

Given a natural number $n$ and a rational $x$, let $B_{n}(x)$ denote the
$n$-th Bernoulli polynomial evaluated at $x$. Then,

$B_{n}(1+x)=B_{n}(x)+nx^{n-1}$

_Natural language proof:_

We apply strong induction on $n$. So, for all $m<d$, we have
$B_{m}(1+x)=B_{m}(x)+mx^{m-1}$ and we want to show that

$B_{d}(1+x)=B_{d}(x)+dx^{d-1}$

Multiplying both sides by $d+1$, and using the fact that, for all
$l\in\mathbb{N}$, $\sum_{k=0}^{l}{l+1\choose k}B_{k}=(l+1)X^{l}$ (where
$B_{k}$ is the $k$-th Bernoulli number), we get that

$(d+1)(1+x)^{d}-(d+1)x^{d}=\sum_{l=0}^{d}{d+1\choose l}lx^{l-1}$

The conclusion then follows easily.

$Q.E.D$

_Codex Output_

Following is the best scored output (proof outline, temperature 0.8) :

Codex Output

⬇

theorem bernoulli_eval_one_add (n : ℕ) (x : ℚ) :

(polynomial.bernoulli n).eval (1 + x) = (polynomial.bernoulli n).eval x + n *
x^(n - 1) :=

begin

– We apply strong induction on $n$. So, for all $m < d$, we have

assume h1 : (∀ m : ℕ, m < n →

(polynomial.bernoulli m).eval (1 + x) = (polynomial.bernoulli m).eval x + m *
x^(m - 1)),

– we want to show that

show (polynomial.bernoulli n).eval (1 + x) = (polynomial.bernoulli n).eval x +
n * x^(n - 1), from begin

– need to use the equation:

– $\sum_{l = 0}^{k} {k + 1 \choose l} B_l = (k + 1) X^k$

have h2 : (∀ k : ℕ, polynomial.C ((k + 1)) * X^k =

polynomial.sum (list.range (k + 1))

(λ (l : ℕ), (polynomial.C (((k + 1) choose l) * (polynomial.bernoulli l))) *
X^l)), from sorry,

– Multiplying both sides by $d + 1$, and using the fact that, for all $l \in
\mathbb{N}$, $\sum_{k = 0}^{l} {l + 1 \choose k} B_k = (l + 1) X^l$, we get
that

have h3 : (polynomial.C ((n + 1)) * (polynomial.C 1 + X)^n).eval x \-

(polynomial.C ((n + 1)) * X^n).eval x =

polynomial.sum (list.range (n + 1))

(λ (l : ℕ), (polynomial.C (((n + 1) choose l))) * (polynomial.C (l * x^(l -
1))))

.eval x, from sorry,

– The conclusion then follows easily.

show (polynomial.bernoulli n).eval (1 + x) = (polynomial.bernoulli n).eval x +
n * x^(n - 1), from sorry,

end,

end

####  D.4.10 The fractional parts of the integer multiples of an irrational
number form a dense subset of the unit interval

This theorem proved to be particularly difficult for Codex to formalise. The
basic constructions in the proof and statement such as _the set of fractional
parts of integer multiples of an irrational number_ were common stumbling
blocks.

The first part of the proof involving showing that the fractional parts of
distinct multiples of an irrational number are distinct – a fact that can be
succintly stated and proved in conventional mathematical notation but can be
quite long when expanded out in full. Some of the full proofs often ran out of
tokens before reaching the rest of the proof. However, full proofs were still
better overall in this case. The performance in both temperatures was
comparable.

Another common error was in the definitions of _limit points_ and _dense
sets_.

We also experimented with adding a correct statement and an extra example
prompt from a related area (the _Sandwich theorem_). Both modifications
resulted in an improvement, suggesting that input-dependent prompting can
improve results of proof autoformalisation as well (though presently not
feasible).

One of the better proof outputs (given below) was an outline at temperature
0.4. (for formatting reasons, ∃ is rendered as ∃ i).

_Theorem statement:_

The fractional parts of the integer multiples of an irrational number form a
dense subset of the unit interval

_Natural language proof:_ Let $\alpha$ be an irrational number. Then for
distinct $i,j\in\mathbb{Z}$, we must have $\\{i\alpha\\}\neq\\{j\alpha\\}$. If
this were not true, then

$i\alpha-\lfloor i\alpha\rfloor=\\{i\alpha\\}=\\{j\alpha\\}=j\alpha-\lfloor
j\alpha\rfloor,$

which yields the false statement $\alpha=\frac{\lfloor i\alpha\rfloor-\lfloor
j\alpha\rfloor}{i-j}\in\mathbb{Q}$. Hence,

$S:=\\{\\{i\alpha\\}\mid i\in\mathbb{Z}\\}$

is an infinite subset of $\left[0,1\right]$.

By the Bolzano-Weierstrass theorem, $S$ has a limit point in $[0,1]$. One can
thus find pairs of elements of $S$ that are arbitrarily close. Since (the
absolute value of) the difference of any two elements of $S$ is also an
element of $S$, it follows that $0$ is a limit point of $S$.

To show that $S$ is dense in $[0,1]$, consider $y\in[0,1]$, and $\epsilon>0$.
Then by selecting $x\in S$ such that $\\{x\\}<\epsilon$ (which exists as $0$
is a limit point), and $N$ such that $N\cdot\\{x\\}\leq y<(N+1)\cdot\\{x\\}$,
we get: $|y-\\{Nx\\}|<\epsilon$. $Q.E.D.$

Codex Output

⬇

theorem irrational_orbit_density (α : ℝ) (h1 : ¬ is_rational α) : dense_set {r | ∃ i : ℤ, r = i*α} :=

begin

–Let $\alpha$ be an irrational number. Then for distinct $i, j \in
\mathbb{Z}$, we must have $\\{i \alpha\\} \neq\\{j \alpha\\}$.

–If this were not true, then $i \alpha-\lfloor i \alpha\rfloor=\\{i
\alpha\\}=\\{j \alpha\\}=j \alpha-\lfloor j \alpha\rfloor$, which yields the
false statement $\alpha=\frac{\lfloor i \alpha\rfloor-\lfloor j
\alpha\rfloor}{i-j} \in \mathbb{Q}$.

have h2 : α ≠ i*α := sorry,

have h3 : ∀ (i j : ℤ), i ≠ j → i*α ≠ j*α, from sorry,

have h4 : ∀ (i j : ℤ), i ≠ j → ¬ (i*α = j*α), from sorry,

– Hence

let S := {r | ∃ (i : ℤ), r = i*α},

have h5 : S ⊆ {r | ∃ (i : ℤ), r = i*α}, from subset.refl S,

have h6 : S = {r | ∃ (i : ℤ), r = i*α}, from set.subset.antisymm h5 h5,

– Consider $y \in[0,1]$, and $\epsilon>0$. Then by selecting $x \in S$ such
that $\\{x\\}<\epsilon$ (which exists as $0$ is a limit point), and $N$ such
that $N \cdot\\{x\\} \leq y<(N+1) \cdot\\{x\\}$, we get: $|y-\\{N
x\\}|<\epsilon$.

have h7 : ∀ (y : ℝ) (ε), y ∈ Icc 0 1 → ε > 0 → ∃ x, x ∈ S ∧ ∃ (N : ℤ), ↑N*(x -
x) ≤ y ∧ y < ↑(N+1)*(x - x) ∧ ↑N*(x - x) - y < ε, from sorry,

– $S$ has a limit point in $[0, 1]$.

have h8 : ∀ (y : ℝ), y ∈ Icc 0 1 → ∃ i (x : ℝ), x ∈ S ∧ dist x y < ε, from
sorry,

– One can thus find pairs of elements of $S$ that are arbitrarily close.

have h9 : ∀ (u : ℝ), ∃ y, y ∈ S ∧ dist u y ≤ dist u y, from sorry,

have h10 : ∀ (y : ℝ) (ε), y ∈ Icc 0 1 → ε > 0 → ∃ x, x ∈ S ∧ dist x y < ε,
from sorry,

– Since (the absolute value of) the difference of any two elements of $S$ is
also an element of $S$, it follows that $0$ is a limit point of $S$.

have h11 : ∀ (x y : ℝ), x ∈ S ∧ y ∈ S → ∃ x’, x’ ∈ S ∧ ∃ (n : ℤ) ∈ set.range
(λ (n : ℤ), (n : ℤ)), n*(x - y) = x’, from sorry,

have h12 : ∀ (y : ℝ) (ε), y ∈ Icc 0 1 → ε > 0 → ∃ x, x ∈ S ∧ dist x y < ε,
from sorry,

– By the Bolzano-Weierstrass theorem, $S$ has a limit point in $[0, 1]$.

have h13 : ∀ (y : ℝ), y ∈ Icc 0 1 → ∃ i (x : ℝ), x ∈ S ∧ dist x y < ε, from
sorry,

have h14 : ∀ (y : ℝ) (ε), y ∈ Icc 0 1 → ε > 0 → ∃ x, x ∈ S ∧ dist x y < ε,
from sorry,

– It follows that $0$ is a limit point of $S$.

have h15 : ∀ (y : ℝ) (ε), y ∈ Icc 0 1 → ε > 0 → ∃ x, x ∈ S ∧ dist x y < ε,
from sorry,

sorry,

end

####  D.4.11 Schur’s lemma

The formalised statement was reasonably accurate in most cases, usually
missing only a few minor details. In some cases, the original statement _f $V$
and $W$ are not isomorphic, then there are no nontrivial representations of
$G$ on $V$ and $W$ respectively_ was translated in the contrapositive as (f :
V -> W) (hf : f ≠ 0) : V ≃ W.

Some common errors were using commutative groups instead of groups, getting
the notion of a representation wrong, and adding several extra assumptions.

Another common mistake that occurred in the statement as well as proofs was
spelling out certain definitions - such as $G$-equivariant maps and the kernel
of a homomorphism - in more detail than needed.

The proof itself is a fairly easy one that follows directly from the
observation that the kernel and image of a module homomorphism are themselves
sub-modules of the domain and codomain respectively. Consequently, the model
has done a fairly good job with formalising this theorem - frequently getting
a score of $3$ on the proofs. The proof variants with comments are often
better structured than their undocumented counterparts.

Schur’s lemma is stated in mathlib, though at an extremely high level of
generality, so chances of contamination from this are minimal. However, we
found a standalone Lean repository containing a proof of Schur’s lemma, which
is a possible source of contamination. We believe that since the proof is
spread across multiple files and is built on definitions introduced within the
repository, direct copying of the proof is unlikely.

_Theorem statement:_

Let $V$ and $W$ be vector spaces; and let $\rho_{V}$ and $\rho_{W}$ be
irreducible representations of $G$ on $V$ and $W$ respectively. If $V$ and $W$
are not isomorphic, then there are no nontrivial representations of $G$ on $V$
and $W$ respectively.

_Natural language proof:_

Suppose $f$ is a nonzero $G$-linear map from $V$ to $W$. We will prove that
$V$ and $W$ are isomorphic. Let $V^{\prime}$ be the kernel, or null space, of
$f$ in $V$, the subspace of all $x$ in $V$ for which $fx=0$. (It is easy to
check that this is a subspace.) By the assumption that $f$ is $G$-linear, for
every $g$ in $G$ and choice of $x$ in
$V^{\prime},f\left(\left(\rho_{V}(g)\right)(x)\right)=\left(\rho_{W}(g)\right)(f(x))=\left(\rho_{W}(g)\right)(0)=0$.
But saying that $f\left(\rho_{V}(g)(x)\right)=0$ is the same as saying that
$\rho_{V}(g)(x)$ is in the null space of $f:V\rightarrow W$. So $V^{\prime}$
is stable under the action of $G$; it is a subrepresentation. Since by
assumption $V$ is irreducible, $V^{\prime}$ must be zero; so $f$ is injective.

By an identical argument we will show $f$ is also surjective; since
$f\left(\left(\rho_{V}(g)\right)(x)\right)=\left(\rho_{W}(g)\right)(f(x))$, we
can conclude that for arbitrary choice of $f(x)$ in the image of
$f,\rho_{W}(g)$ sends $f(x)$ somewhere else in the image of $f$; in particular
it sends it to the image of $\rho_{V}(g)x$. So the image of $f(x)$ is a
subspace $W^{\prime}$ of $W$ stable under the action of $G$, so it is a
subrepresentation and $f$ must be zero or surjective. By assumption it is not
zero, so it is surjective, in which case it is an isomorphism.

$Q.E.D.$

_Codex Output_

⬇

theorem schurs_lemma {G : Type*} {V W : Type*} [group G] [add_comm_group V]
[add_comm_group W] [vector_space ℂ V] [vector_space ℂ W] [module ℂ G V]
[module ℂ G W] [irreducible G V] [irreducible G W] (f : V →[ℂ] W) : f ≠ 0 → V
≃ W :=

begin

– Suppose $f$ is a nonzero $G$-linear map from $V$ to $W$. We will prove that
$V$ and $W$ are isomorphic.

assume h1 : f ≠ 0,

have h1a : f ≠ 0, from show f ≠ 0, from by auto [h1, zero_smul] using
[linear_map.map_zero],

have h1b : f ≠ 0, from show f ≠ 0, from by auto [h1, smul_zero] using
[linear_map.map_zero],

– Let $V^{\prime}$ be the kernel, or null space, of $f$ in $V$, the subspace
of all $x$ in $V$ for which $f x=0$. (It is easy to check that this is a
subspace.)

let V’ : set V := ker f,

have h2 : V’ ⊆ V, from by auto [linear_map.ker_subset],

– By the assumption that $f$ is $G$-linear, for every $g$ in $G$ and choice of
$x$ in $V^{\prime},
f\left(\left(\rho_V(g)\right)(x)\right)=\left(\rho_W(g)\right)(f(x))=\left(\rho_W(g)\right)(0)=0$.

have h3 : ∀ g : G, ∀ x : V, x ∈ V’ → f (g • x) = 0, from by auto
[linear_map.mem_ker] using [linear_map.map_smul],

have h4 : ∀ g : G, ∀ x : V, x ∈ V’ → f (g • x) = 0, from by auto [h3] using
[linear_map.map_smul],

– But saying that $f\left(\rho_V(g)(x)\right)=0$ is the same as saying that
$\rho_V(g)(x)$ is in the null space of $f: V \rightarrow W$.

have h5 : ∀ g : G, ∀ x : V, x ∈ V’ → g • x ∈ V’, from by auto [h3, mem_ker]
using [linear_map.map_smul, linear_map.map_zero],

– So $V^{\prime}$ is stable under the action of $G$; it is a
subrepresentation.

have h6 : subrepresentation G V V’, from subrepresentation.mk’ (h5 : _),

have h7 : is_submodule G V’ V, from is_submodule.mk (h5 : _),

– Since by assumption $V$ is irreducible, $V^{\prime}$ must be zero; so $f$ is
injective.

have h8 : irreducible G V’ → V’ = (linear_map.ker f), from by auto
[irreducible.irr_ker_eq, h1a, h1b] using [linear_map.map_zero],

have h9 : irreducible G (V’) → (V’) = (0), from by auto
[irreducible.irr_eq_zero, h1a, h1b, h8, linear_map.ker_eq_zero] using
[linear_map.map_zero],

have h10 : irreducible G (V’) → (V’) = (0), from by auto [h9, h6,
irreducible_subrepresentation],

have h11 : irreducible G (V’) → (V’) = (0), from by auto [h10,
irreducible_subrepresentation],

have h12 : V’ = 0, from by auto [h11],

– By an identical argument we will show $f$ is also surjective;

have h13 : linear_map.range f ⊆ W, from by auto [linear_map.range_subset_iff],

have h14 : linear_map.range f ⊆ W, from by auto [h13,
linear_map.range_subset_iff],

have h15 : ∀ g : G, ∀ x : V, x ∈ linear_map.range f → g • x ∈ linear_map.range
f, from by auto [linear_map.mem_range, linear_map.map_smul] using
[linear_map.map_smul],

have h16 : subrepresentation G W (linear_map.range f), from
subrepresentation.mk’ (h15 : _),

have h17 : is_submodule G (linear_map.range f) W, from is_submodule.mk (h15 :
_),

– since
$f\left(\left(\rho_V(g)\right)(x)\right)=\left(\rho_W(g)\right)(f(x))$, we can
conclude that for arbitrary choice of $f(x)$ in the image of $f, \rho_W(g)$
sends $f(x)$ somewhere else in the image of $f; in particular it sends it to
the image of $\rho_V(g) x$.

have h18 : ∀ g : G, ∀ v : V, v ∈ linear_map.range f → g • v ∈ linear_map.range
f, from by auto [linear_map.mem_range, linear_map.map_smul] using
[linear_map.map_smul],

have h19 : subrepresentation G W (linear_map.range f), from
subrepresentation.mk’ (h18 : _),

have h20 : is_submodule G (linear_map.range f) W, from is_submodule.mk (h18 :
_),

– So the image of $f(x)$ is a subspace $W^{\prime}$ of $W$ stable under the
action of $G$, so it is a subrepresentation and $f$ must be zero or
surjective.

have h21 : is_submodule G (linear_map.range f) W → linear_map.range f = W → f
≠ 0, from by auto [linear_map.range_eq_top],

have h22 : is_submodule G (linear_map.range f) W → linear_map.range f = W → f
≠ 0, from by auto [h21, h20] using [linear_map.injective],

have h23 : is_submodule G (linear_map.range f) W → linear_map.range f = W → f
≠ 0, from by auto [h22, linear_map.injective_eq_range_eq_top] using
[linear_map.injective],

have h24 : is_submodule G (linear_map.range f) W → linear_map.range f = W → f
≠ 0, from by auto [h23, h16] using [irreducible_subrepresentation],

– By assumption it is not zero, so it is surjective, in which case it is an
isomorphism.

have h25 : f ≠ 0 → linear_map.range f = W, from by auto [h24, h1b] using
[linear_map.range_eq_top],

have h26 : f ≠ 0 → linear_map.range f = W, from by auto [h25, h12] using
[linear_map.range_eq_top],

– QED

show f ≠ 0 → V ≃ W, from by auto [linear_map.is_linear_equiv, h26] using
[linear_map.is_linear_equiv]

end

####  D.4.12 A graph is bipartite iff it is $2$-colourable

The scores for the statement formalisation were overall very low - the most
common formalisation was two_colorable G ↔ bipartite G, which is incorrect as
neither of these terms are defined in mathlib. The proof outlines and outlines
with auto were also of low quality, often failing to split the proof into two
cases and failing to explicitly define the two parts in the bipartite graph.
Full proofs seem to be doing marginally better, with outlines being the second
best. Although the average performances in temperatures 0.4 and 0.8 are the
same, the maximum scores are attained at temperature 0.8.

The best proof format observed were outlines at temperature 0.8. Correct Lean
theorem statement was not included in the prompt.

_Theorem statement:_

Let $G$ be a graph. Then $G$ is 2-colorable if and only if $G$ is bipartite.

_Natural language proof:_

Let $G$ be a 2-colorable graph, which means we can color every vertex either
red or blue, and no edge will have both endpoints colored the same color. Let
$A$ denote the subset of vertices colored red, and let $B$ denote the subset
of vertices colored blue. Since all vertices of $A$ are red, there are no
edges within $A$, and similarly for $B$. This implies that every edge has one
endpoint in $A$ and the other in $B$, which means $G$ is bipartite.

Conversely, suppose $G$ is bipartite, that is, we can partition the vertices
into two subsets $V_{1},V_{2}$ every edge has one endpoint in $V_{1}$ and the
other in $V_{2}$. Then coloring every vertex of $V_{1}$ red and every vertex
of $V_{2}$ blue yields a valid coloring, so $G$ is 2-colorable.

$Q.E.D.$

_Codex Output_

⬇

theorem graph_2_colorable_iff_bipartite : ∀ G : graph, (∃ c : coloring G 2,
is_valid_coloring G c) ↔ is_bipartite G := begin – Let $G$ be a 2-colorable
graph, which means we can color every vertex either red or blue, – and no edge
will have both endpoints colored the same color. assume (G : graph), have h1 :
∀ c : coloring G 2, (is_valid_coloring G c), from

by {

assume (c : coloring G 2),

sorry,

},

– Let $A$ denote the subset of vertices colored red, and let $B$ denote the
subset of vertices colored blue.

have h2 : ∀ c : coloring G 2, (is_valid_coloring G c) → (∃ A : set (vertex G),
∃ B : set (vertex G), (∀ v : vertex G, c v = red ↔ v ∈ A) ∧ (∀ v : vertex G, c
v = blue ↔ v ∈ B)), from by assume (c : coloring G 2) (h2 :is_valid_coloring G
c),

sorry,

},

– $A$ and $B$ are subsets of vertics of $G$, by definition of valid coloring.

have h3 : ∀ c : coloring G 2, (is_valid_coloring G c) → (∃ A : set (vertex G),
∃ B : set (vertex G), (∀ v : vertex G, c v = red ↔ v ∈ A) ∧ (∀ v : vertex G, c
v = blue ↔ v ∈ B) ∧ A ⊆ vertex G ∧ B ⊆ vertex G), from by assume (c : coloring
G 2) (h3 :is_valid_coloring G c),

sorry,

},

– Since all vertices of $A$ are red, there are no edges within $A$,

– and similarly for $B$.

have h4 : ∀ c : coloring G 2, (is_valid_coloring G c) → (∃ A : set (vertex G),
∃ B : set (vertex G), (∀ v : vertex G, c v = red ↔ v ∈ A) ∧ (∀ v : vertex G, c
v = blue ↔ v ∈ B) ∧ A ⊆ vertex G ∧ B ⊆ vertex G ∧ ∀ e : edge G, (source e ∈ A
∧ target e ∈ A) ∨ (source e ∈ B ∧ target e ∈ B)), from by assume (c : coloring
G 2) (h4 :is_valid_coloring G c),

sorry,

},

– This implies that every edge has one endpoint in $A$ and the other in $B$,

– which means $G$ is bipartite.

have h5 : ∀ c : coloring G 2, (is_valid_coloring G c) → (∃ A : set (vertex G),
∃ B : set (vertex G), (∀ v : vertex G, c v = red ↔ v ∈ A) ∧ (∀ v : vertex G, c
v = blue ↔ v ∈ B) ∧ A ⊆ vertex G ∧ B ⊆ vertex G ∧ (∀ e : edge G, source e ∈ A
∨ source e ∈ B) ∧ (∀ e : edge G, target e ∈ A ∨ target e ∈ B)), from by assume
(c : coloring G 2) (h5 :is_valid_coloring G c),

sorry,

},

– Hence the existence of a valid coloring implies that the graph is bipartite.

have h6 : ∀ c : coloring G 2, (is_valid_coloring G c) → (∃ A : set (vertex G),
∃ B : set (vertex G), (∀ v : vertex G, c v = red ↔ v ∈ A) ∧ (∀ v : vertex G, c
v = blue ↔ v ∈ B) ∧ A ⊆ vertex G ∧ B ⊆ vertex G ∧ A ⊥ B ∧ A ∪ B = vertex G),
from by assume (c : coloring G 2) (h6 :is_valid_coloring G c),

sorry,

},

– Conversely,

have h7 : ∀ A B : set (vertex G), A ⊥ B → A ⊆ vertex G ∧ B ⊆ vertex G → A ∪ B
= vertex G →

(∃ c : coloring G 2, is_valid_coloring G c ∧

(∀ v : vertex G, c v = red ↔ v ∈ A) ∧ (∀ v : vertex G, c v = blue ↔ v ∈ B)),
from

by {

assume (A B : set (vertex G)) (h7 : A ⊥ B) (h8 : A ⊆ vertex G ∧ B ⊆ vertex G)
(h9 : A ∪ B = vertex G),

sorry,

},

– Suppose $G$ is bipartite,

have h8 : ∀ A B : set (vertex G), A ⊥ B → A ⊆ vertex G ∧ B ⊆ vertex G → A ∪ B
= vertex G →

is_bipartite G, from

by {

assume (A B : set (vertex G)) (h8 : A ⊥ B) (h9 : A ⊆ vertex G ∧ B ⊆ vertex G)
(h10 : A ∪ B = vertex G),

sorry,

},

– Hence the existence of a valid coloring is equivalent to the graph being
bipartite.

sorry,

end

####  D.4.13 p-adic units

In a few cases, Codex ignored the _p-adic_ setting entirely and formalised
everything in terms of integers and natural numbers. The correct notation for
p-adic integers was also not captured correctly in most cases. A common error
was to formalise the first line of the proof (”Let us prove the
contrapositive, that is, is $x$ is not a unit of $\mathbb{Z}_{p}$, then $x$ is
not coprime to $p$.”), which outlined the general strategy of the proof, as a
separate have statement. Proofs with premises were by far the best, with
fairly useful outlines and relevant-looking theorem names in the arguments for
auto. The results seem to be better at temperature 0.4.

This proof is entirely uncontaminated.

_Theorem statement:_

Given a prime number $p$ and a natural number $x$, if $x$ is coprime to $p$,
then $x$ is a unit in the $p$-adic integers.

_Natural language proof:_ Let us prove the contrapositive, that is, is $x$ is
not a unit of $\mathbb{Z}_{p}$, then $x$ is not coprime to $p$. We know that
any element of $\mathbb{Z}_{p}$ is a unit if and only if it has norm 1, thus
$\|x\|\neq 1$. Also, since every element of $\mathbb{Z}_{p}$ must have norm
less than or equal to 1, we conclude that $\|x\|<1$. But this must imply that
$p|x$. This completes our proof.

$Q.E.D.$

_Codex Output_

One of the best outputs (proof with premises, temperature 0.4):

⬇

theorem p_adic_units (p : ℕ) (x : ℕ) (h : coprime p x) : is_unit (x : ℤ/p) :=

begin

– Prove the contrapositive, that is, is $x$ is not a unit of $\mathbb{Z}_p$,
then $x$ is not coprime to $p$

have h1 : ¬ is_unit (x : ℤ/p) → ¬ coprime p x, from by auto [nat.coprime.symm,
nat.coprime.def, nat.coprime.def, nat.coprime.symm, nat.coprime.def,
nat.coprime.def],

– We know that any element of $\mathbb{Z}_p$ is a unit if and only if it has
norm 1

have h2 : is_unit (x : ℤ/p) ↔ (norm_num (x : ℤ/p)) = 1, from by auto
[norm_num_eq_one_iff_is_unit],

– Also, since every element of $\mathbb{Z}_p$ must have norm less than or
equal to 1

have h3 : (norm_num (x : ℤ/p)) ≤ 1, from by auto [norm_num_le_one],

– But this must imply that $p | x$

have h4 : ¬ is_unit (x : ℤ/p) → p | x, from by auto [norm_num_eq_one_iff_is_unit, norm_num_le_one, nat.dvd_iff_norm_num_eq_zero],

– This completes our proof

show is_unit (x : ℤ/p), from by auto [h1, h2, h3, h4, h]

end