Derivations, CAS, Lean, and Assumptions in Physics

Initially the Physics Derivation Graph documented expressions as Latex. Then SymPy was added to support validation of steps (is the step self-consistent) and dimensionality (is the expression self-consistent?). 

Recently I learned that Lean could be used to prove each step in a derivation. The difference between a Computer Algebra System (e.g., SymPy) and Lean is whether "a = b  --> a/b = 1" is a valid step -- it isn't when b is zero. Lean catches that; SymPy does not. 

While Lean proofs sound like the last possible refinement, there are two additional complications to account for not addressed by Lean. 

Challenge: Bounded ranges of applicability

In classical mechanics the relation between momentum, mass, and velocity is "p = m v". That hold when "v << c". Near the speed of light we need to switch to relativistic mass, 

m = m_{rest} / sqrt{1-((v^2)/(c^2))}.

The boundary between "v << c" and "v ~ c" is usually set by the context being considered. 

One response for users of Lean would be to always use the "correct" relativistic equation, even when "v << c."  A more conventional approach used by Physicists is to use

p = m v, where v << c

then drop the "v << c" clause and rely on context.

Challenge: Real versus Float versus experimental characterization

Lean forces you to characterize numbers as Real or Integer or Complex. This presents a problem for numerical simulations that have something like a 64 bit float representation.

In thermodynamics we assume the number of particles involved is sufficiently large that we focus on the behavior of the ensemble rather than individual particles. The imprecision of floats is not correct, but neither is the infinite precision assumed by Real numbers. 

Example applications of Lean proofs needing bounds on values

Math doesn't have convenient ways of indicating "finite precision, as set by the Plank scale."  The differential element used in calculus cannot actually go to zero, but we use that concept because it works at the scales we are used to. 

Physicists make simplifying assumptions that sometimes ignore reality (e.g., assuming continuous media when particles are discrete). Then again the assumption that particles are discrete is also a convenient fiction that ignores the wavefunction of quantum mechanics. 

Lean can be used to prove derivations in classical mechanics, but to be explicit about the bounds of those proofs we'd also need to indicate "v << c" and "assume space is Euclidean." 

For molecular dynamics, another constraint to account for is "temperature << 1E10 Kelvin" or whatever temperature the atoms breaks down into plasma. 

Distinguishing the context of (classical mechanics from quantum) and (classical from relativistic) and (conventional gas versus plasma) seems important so that we know when a claim proven in Lean is applicable. 

dichotomy of assumptions

In Physics there are some assumptions that form a dichotomy:

• is the speed of light constant or variable?
• is the measure of energy discrete or continuous?

In the dichotomy of assumptions, one of the two assumptions is reflective of reality, and the other is an oversimplification. The oversimplification is related to reality by assumptions, constraints, and limits. 

(I define "oversimplification" as the extension of useful assumptions to incorrect regions.)

Another case where oversimplification is the link between domains is quantum physics and (classical) statistical physics. Quantum particles are either Fermions (odd half integer spin) or Bosons (integer spin), but that is practically irrelevant for large ensembles of particles at room temperature. The aspects that get measured at one scale (e.g., particle velocity) are related to but separate from metrics at another scale (e.g, temperature, entropy). Mathematically this transition manifests as the switch from summation to integration.

So what? 
This is a new-to-me category of derivations which span domains. What constitutes a domain is set by the assumptions that form the boundaries, and oversimplification is how to cross the boundaries. 

What boundaries should the Physics Derivation Graph transgress? What oversimplifications are adjacent?

• quantum mechanics to classical - https://en.wikipedia.org/wiki/Canonical_quantization
• https://en.wikipedia.org/wiki/Optics
• https://en.wikipedia.org/wiki/Condensed_matter_physics
• https://en.wikipedia.org/wiki/Statistical_mechanics
• https://scholar.harvard.edu/files/schwartz/files/10-quantumstatmech_0.pdf
• https://physics.stackexchange.com/questions/374647/for-ideal-classical-gasses-in-terms-of-the-energy-levels-why-do-we-ignore-wheth
• relativity to classical
• https://en.wikipedia.org/wiki/Astrometry
• https://en.wikipedia.org/wiki/Orbital_mechanics
• https://en.wikipedia.org/wiki/Celestial_mechanics
• https://en.wikipedia.org/wiki/Galactic_astronomy
• https://en.wikipedia.org/wiki/Astronomy#Stellar_astronomy
• https://physics.stackexchange.com/questions/580494/difference-between-relativistic-and-non-relativistic-classical-equations-of-elec
• "The EFE reduce to Newton's law of gravity by using both the weak-field approximation and the slow-motion approximation." source
• quantum field theory to quantum mechanics
• https://en.wikipedia.org/wiki/Quantum_field_theory#Mathematical_rigor -- see particle in a box

The evidences of dissonance (e.g, Mercury’s perihelion based on Newtonian gravitation versus relativity, the Deflection of Starlight; source) are not relevant for bridging domains. They are illustrations of the oversimplification.

Update 2024-03-10: on the page https://en.wikipedia.org/wiki/Phase_space#Quantum_mechanics

"by expressing quantum mechanics in phase space (the same ambit as for classical mechanics), the Weyl map facilitates recognition of quantum mechanics as a deformation (generalization) of classical mechanics, with deformation parameter ħ/S, where S is the action of the relevant process. (Other familiar deformations in physics involve the deformation of classical Newtonian into relativistic mechanics, with deformation parameter v/c; or the deformation of Newtonian gravity into general relativity, with deformation parameter Schwarzschild radius/characteristic dimension.)
 
Classical expressions, observables, and operations (such as Poisson brackets) are modified by ħ-dependent quantum corrections, as the conventional commutative multiplication applying in classical mechanics is generalized to the noncommutative star-multiplication characterizing quantum mechanics and underlying its uncertainty principle."

See also https://en.wikipedia.org/wiki/Wigner%E2%80%93Weyl_transform#Deformation_quantization

derivations, identities, and other categories of mathematical physics

Transforming from one expression to another is carried out with respect to a goal. There are different categories of goals (listed below). I don't yet know what distinguishes one category from another.

My motivation for the Physics Derivation Graph is exclusively the first category -- derivations, specifically across domains. This motivation is more specific than a broader question, "what is the relation between every expression in mathematical physics and every other expression?" because the answer might be "symbols and inference rules are common."

The other categories are neat but not as rewarding for me. These other categories are included in the PDG because the infrastructure for software and UI and data format are the same.

Examples of Derivations

Relation between two disparate descriptions of nature:

• Maxwell equations to electric field wave equation
• optics: Law of refraction to Brewster's angle

Derivation of expression from simpler observations plus assumptions:

• Newton's Law of Gravitation
• first law of thermodynamics

An expression in one domain simplifies to another expression in a different domain under modified assumptions

• https://en.wikipedia.org/wiki/Correspondence_principle
• https://www.physicsforums.com/threads/schroedinger-equation-in-the-classical-limit.775531/
• https://mathoverflow.net/questions/102313/classical-limit-of-quantum-mechanics
• "A wave equation interpolating between classical and quantum mechanics"
• https://mathoverflow.net/questions/225814/does-quantum-mechanics-ever-really-quantize-classical-mechanics
• https://farside.ph.utexas.edu/teaching/sm1/lectures/node82.html

The same concept appears in multiple domains

• Anderson localization (for electron transport, photonics; anywhere with waves)
• simple harmonic oscillator, particle in a box
• https://en.wikipedia.org/wiki/Continuity_equation, aka transport equation

Examples of Identities

An equation can be expressed differently but be equivalent:

• Euler equation: trig square root

Examples of Proofs

Show that two sides of an equation are, in fact, the same:

• Euler equation proof

Examples of Use Case

Start from one or more expressions to derive a conclusion with practical utility

• escape velocity
• Schwarzschild radius for non-rotating black hole
• angle of maximum distance for projectile motion
• speed of Earth around Sun
• mass of the Earth

This is the focus of the ATOMS lab at UMBC, specifically enacted using Lean.

Python dependencies visualization using pydeps

To see what Python modules are available on my system I can run

pydoc3 modules

One of the modules is pandas. Here's a script that just loads pandas module:

cat load_pandas.py 
import warnings
warnings.filterwarnings("ignore", category=DeprecationWarning)
import pandas as pd 

When the script is run nothing happens

python3 load_pandas.py

I have pydeps installed:

pydeps --version
pydeps v1.12.17

Output of analysis by pydeps:

pydeps -o myfile.png --show-dot -T png --noshow load_pandas.py 

digraph G {
    concentrate = true;

    rankdir = TB;
    node [style=filled,fillcolor="#ffffff",fontcolor="#000000",fontname=Helvetica,fontsize=10];

    load_pandas_py [fillcolor="#a65959",fontcolor="#ffffff",label="load_pandas.py"];
    pandas [fillcolor="#039595",fontcolor="#ffffff"];
    pandas__config [fillcolor="#24d0d0",label="pandas._config"];
    pandas__version [fillcolor="#47c2c2",label="pandas\.\n_version"];
    pandas__version_meson [fillcolor="#47c2c2",label="pandas\.\n_version_meson"];
    pandas_api [fillcolor="#3db8b8",label="pandas.api"];
    pandas_arrays [fillcolor="#46a4a4",label="pandas.arrays"];
    pandas_compat [fillcolor="#17d3d3",label="pandas.compat"];
    pandas_compat__optional [fillcolor="#31c4c4",label="pandas\.\ncompat\.\n_optional"];
    pandas_compat_pyarrow [fillcolor="#3db8b8",label="pandas\.\ncompat\.\npyarrow"];
    pandas_core [fillcolor="#10f9f9",label="pandas.core"];
    pandas_core_api [fillcolor="#3a8888",fontcolor="#ffffff",label="pandas\.\ncore\.\napi"];
    pandas_core_computation [fillcolor="#3bcece",label="pandas\.\ncore\.\ncomputation"];
    pandas_core_computation_api [fillcolor="#46a4a4",label="pandas\.\ncore\.\ncomputation\.\napi"];
    pandas_core_config_init [fillcolor="#3a8888",fontcolor="#ffffff",label="pandas\.\ncore\.\nconfig_init"];
    pandas_core_dtypes [fillcolor="#2fdbdb",label="pandas\.\ncore\.\ndtypes"];
    pandas_core_dtypes_dtypes [fillcolor="#339999",fontcolor="#ffffff",label="pandas\.\ncore\.\ndtypes\.\ndtypes"];
    pandas_core_reshape [fillcolor="#47c2c2",label="pandas\.\ncore\.\nreshape"];
    pandas_core_reshape_api [fillcolor="#46a4a4",label="pandas\.\ncore\.\nreshape\.\napi"];
    pandas_errors [fillcolor="#3ab0b0",label="pandas.errors"];
    pandas_io [fillcolor="#0bdfdf",label="pandas.io"];
    pandas_io_api [fillcolor="#46a4a4",label="pandas.io.api"];
    pandas_io_json [fillcolor="#23c8c8",label="pandas.io.json"];
    pandas_io_json__normalize [fillcolor="#4cb3b3",label="pandas\.\nio\.\njson\.\n_normalize"];
    pandas_plotting [fillcolor="#31c4c4",label="pandas\.\nplotting"];
    pandas_testing [fillcolor="#4cb3b3",label="pandas.testing"];
    pandas_tseries [fillcolor="#23c8c8",label="pandas.tseries"];
    pandas_tseries_api [fillcolor="#46a4a4",label="pandas\.\ntseries\.\napi"];
    pandas_tseries_offsets [fillcolor="#26d9d9",label="pandas\.\ntseries\.\noffsets"];
    pandas_util [fillcolor="#05e5e5",label="pandas.util"];
    pandas_util__print_versions [fillcolor="#409696",fontcolor="#ffffff",label="pandas\.\nutil\.\n_print_versions"];
    pandas_util__tester [fillcolor="#46a4a4",label="pandas\.\nutil\.\n_tester"];
    pandas -> load_pandas_py [fillcolor="#039595",minlen="2"];
    pandas__config -> pandas [fillcolor="#24d0d0"];
    pandas__config -> pandas_core_config_init [fillcolor="#24d0d0",minlen="2"];
    pandas__config -> pandas_errors [fillcolor="#24d0d0"];
    pandas__version -> pandas [fillcolor="#47c2c2"];
    pandas__version -> pandas_util__print_versions [fillcolor="#47c2c2",minlen="2"];
    pandas__version_meson -> pandas [fillcolor="#47c2c2"];
    pandas__version_meson -> pandas_util__print_versions [fillcolor="#47c2c2",minlen="2"];
    pandas_api -> pandas [fillcolor="#3db8b8"];
    pandas_arrays -> pandas [fillcolor="#46a4a4"];
    pandas_compat -> pandas [fillcolor="#17d3d3"];
    pandas_compat -> pandas_core_dtypes_dtypes [fillcolor="#17d3d3",minlen="3"];
    pandas_compat -> pandas_util__print_versions [fillcolor="#17d3d3",minlen="2"];
    pandas_compat -> pandas_util__tester [fillcolor="#17d3d3",minlen="2"];
    pandas_compat__optional -> pandas [fillcolor="#31c4c4",minlen="2"];
    pandas_compat__optional -> pandas_util__print_versions [fillcolor="#31c4c4",minlen="2"];
    pandas_compat__optional -> pandas_util__tester [fillcolor="#31c4c4",minlen="2"];
    pandas_compat_pyarrow -> pandas [fillcolor="#3db8b8",minlen="2"];
    pandas_compat_pyarrow -> pandas_compat [fillcolor="#3db8b8",weight="2"];
    pandas_core -> pandas [fillcolor="#10f9f9"];
    pandas_core -> pandas_arrays [fillcolor="#10f9f9"];
    pandas_core -> pandas_util [fillcolor="#10f9f9"];
    pandas_core_api -> pandas [fillcolor="#3a8888",minlen="2"];
    pandas_core_computation -> pandas [fillcolor="#3bcece",minlen="2"];
    pandas_core_computation -> pandas_core_config_init [fillcolor="#3bcece",weight="2"];
    pandas_core_computation_api -> pandas [fillcolor="#46a4a4",minlen="3"];
    pandas_core_config_init -> pandas [fillcolor="#3a8888",minlen="2"];
    pandas_core_dtypes -> pandas [fillcolor="#2fdbdb",minlen="2"];
    pandas_core_dtypes -> pandas_core_api [fillcolor="#2fdbdb",weight="2"];
    pandas_core_dtypes -> pandas_core_config_init [fillcolor="#2fdbdb",weight="2"];
    pandas_core_dtypes_dtypes -> pandas [fillcolor="#339999",minlen="3"];
    pandas_core_dtypes_dtypes -> pandas_core_api [fillcolor="#339999",minlen="2",weight="2"];
    pandas_core_reshape -> pandas [fillcolor="#47c2c2",minlen="2"];
    pandas_core_reshape_api -> pandas [fillcolor="#46a4a4",minlen="3"];
    pandas_errors -> pandas [fillcolor="#3ab0b0"];
    pandas_errors -> pandas_core_dtypes_dtypes [fillcolor="#3ab0b0",minlen="3"];
    pandas_io -> pandas [fillcolor="#0bdfdf"];
    pandas_io -> pandas_core_api [fillcolor="#0bdfdf",minlen="2"];
    pandas_io -> pandas_core_config_init [fillcolor="#0bdfdf",minlen="2"];
    pandas_io_api -> pandas [fillcolor="#46a4a4",minlen="2"];
    pandas_io_json -> pandas [fillcolor="#23c8c8",minlen="2"];
    pandas_io_json -> pandas_io [fillcolor="#23c8c8",weight="2"];
    pandas_io_json -> pandas_io_api [fillcolor="#23c8c8",weight="2"];
    pandas_io_json__normalize -> pandas [fillcolor="#4cb3b3",minlen="3"];
    pandas_plotting -> pandas [fillcolor="#31c4c4"];
    pandas_plotting -> pandas_core_config_init [fillcolor="#31c4c4",minlen="2"];
    pandas_testing -> pandas [fillcolor="#4cb3b3"];
    pandas_tseries -> pandas [fillcolor="#23c8c8"];
    pandas_tseries -> pandas_core_api [fillcolor="#23c8c8",minlen="2"];
    pandas_tseries_api -> pandas [fillcolor="#46a4a4",minlen="2"];
    pandas_tseries_offsets -> pandas [fillcolor="#26d9d9",minlen="2"];
    pandas_tseries_offsets -> pandas_core_api [fillcolor="#26d9d9",minlen="2"];
    pandas_tseries_offsets -> pandas_tseries [fillcolor="#26d9d9",weight="2"];
    pandas_tseries_offsets -> pandas_tseries_api [fillcolor="#26d9d9",weight="2"];
    pandas_util -> pandas [fillcolor="#05e5e5"];
    pandas_util -> pandas_arrays [fillcolor="#05e5e5"];
    pandas_util -> pandas_compat__optional [fillcolor="#05e5e5",minlen="2"];
    pandas_util -> pandas_compat_pyarrow [fillcolor="#05e5e5",minlen="2"];
    pandas_util -> pandas_core_dtypes_dtypes [fillcolor="#05e5e5",minlen="3"];
    pandas_util -> pandas_errors [fillcolor="#05e5e5"];
    pandas_util__print_versions -> pandas [fillcolor="#409696",minlen="2"];
    pandas_util__tester -> pandas [fillcolor="#46a4a4",minlen="2"];
}

LLM that includes the concept of inference rules

Question: What's the difference between a plain old search engine and an LLM+RAG?
Answer: LLM+RAG provides an experience like semantic search capability plus synthesis but without the need for semantic tagging on the front-end or the back-end. 
[https://www.sbert.net/examples/applications/semantic-search/README.html#semantic-search]

Relevance to the Physics Derivation Graph: add the following to an existing large language model (LLM)

• the list of inference rules for the Physics Derivation Graph
• examples of Latex-to-Sage conversion
• example Lean4 proofs

"fine tuning" versus "context provision"

How is "context provision" different from RAG?

What's the difference between a transformer and a model?

https://huggingface.co/docs/transformers/main/model_doc/llama2

https://huggingface.co/meta-llama

specifically

https://huggingface.co/meta-llama/Llama-2-7b-chat

output of help for llama.cpp

docker run -it --rm  -v `pwd`:/scratch llama-cpp-with-mistral-7b-v0.1.q6_k:2023-12-22 /bin/bash 
root@dc98ac4a23d5:/opt/llama.cpp# ./main -h

usage: ./main [options]

options:
  -h, --help            show this help message and exit
      --version         show version and build info
  -i, --interactive     run in interactive mode
  --interactive-first   run in interactive mode and wait for input right away
  -ins, --instruct      run in instruction mode (use with Alpaca models)
  -cml, --chatml        run in chatml mode (use with ChatML-compatible models)
  --multiline-input     allows you to write or paste multiple lines without ending each in '\'
  -r PROMPT, --reverse-prompt PROMPT
                        halt generation at PROMPT, return control in interactive mode
                        (can be specified more than once for multiple prompts).
  --color               colorise output to distinguish prompt and user input from generations
  -s SEED, --seed SEED  RNG seed (default: -1, use random seed for < 0)
  -t N, --threads N     number of threads to use during generation (default: 20)
  -tb N, --threads-batch N
                        number of threads to use during batch and prompt processing (default: same as --threads)
  -p PROMPT, --prompt PROMPT
                        prompt to start generation with (default: empty)
  -e, --escape          process prompt escapes sequences (\n, \r, \t, \', \", \\)
  --prompt-cache FNAME  file to cache prompt state for faster startup (default: none)
  --prompt-cache-all    if specified, saves user input and generations to cache as well.
                        not supported with --interactive or other interactive options
  --prompt-cache-ro     if specified, uses the prompt cache but does not update it.
  --random-prompt       start with a randomized prompt.
  --in-prefix-bos       prefix BOS to user inputs, preceding the `--in-prefix` string
  --in-prefix STRING    string to prefix user inputs with (default: empty)
  --in-suffix STRING    string to suffix after user inputs with (default: empty)
  -f FNAME, --file FNAME
                        prompt file to start generation.
  -n N, --n-predict N   number of tokens to predict (default: -1, -1 = infinity, -2 = until context filled)
  -c N, --ctx-size N    size of the prompt context (default: 512, 0 = loaded from model)
  -b N, --batch-size N  batch size for prompt processing (default: 512)
  --samplers            samplers that will be used for generation in the order, separated by ';', for example: "top_k;tfs;typical;top_p;min_p;temp"
  --sampling-seq        simplified sequence for samplers that will be used (default: kfypmt)
  --top-k N             top-k sampling (default: 40, 0 = disabled)
  --top-p N             top-p sampling (default: 0.9, 1.0 = disabled)
  --min-p N             min-p sampling (default: 0.1, 0.0 = disabled)
  --tfs N               tail free sampling, parameter z (default: 1.0, 1.0 = disabled)
  --typical N           locally typical sampling, parameter p (default: 1.0, 1.0 = disabled)
  --repeat-last-n N     last n tokens to consider for penalize (default: 64, 0 = disabled, -1 = ctx_size)
  --repeat-penalty N    penalize repeat sequence of tokens (default: 1.1, 1.0 = disabled)
  --presence-penalty N  repeat alpha presence penalty (default: 0.0, 0.0 = disabled)
  --frequency-penalty N repeat alpha frequency penalty (default: 0.0, 0.0 = disabled)
  --mirostat N          use Mirostat sampling.
                        Top K, Nucleus, Tail Free and Locally Typical samplers are ignored if used.
                        (default: 0, 0 = disabled, 1 = Mirostat, 2 = Mirostat 2.0)
  --mirostat-lr N       Mirostat learning rate, parameter eta (default: 0.1)
  --mirostat-ent N      Mirostat target entropy, parameter tau (default: 5.0)
  -l TOKEN_ID(+/-)BIAS, --logit-bias TOKEN_ID(+/-)BIAS
                        modifies the likelihood of token appearing in the completion,
                        i.e. `--logit-bias 15043+1` to increase likelihood of token ' Hello',
                        or `--logit-bias 15043-1` to decrease likelihood of token ' Hello'
  --grammar GRAMMAR     BNF-like grammar to constrain generations (see samples in grammars/ dir)
  --grammar-file FNAME  file to read grammar from
  --cfg-negative-prompt PROMPT
                        negative prompt to use for guidance. (default: empty)
  --cfg-negative-prompt-file FNAME
                        negative prompt file to use for guidance. (default: empty)
  --cfg-scale N         strength of guidance (default: 1.000000, 1.0 = disable)
  --rope-scaling {none,linear,yarn}
                        RoPE frequency scaling method, defaults to linear unless specified by the model
  --rope-scale N        RoPE context scaling factor, expands context by a factor of N
  --rope-freq-base N    RoPE base frequency, used by NTK-aware scaling (default: loaded from model)
  --rope-freq-scale N   RoPE frequency scaling factor, expands context by a factor of 1/N
  --yarn-orig-ctx N     YaRN: original context size of model (default: 0 = model training context size)
  --yarn-ext-factor N   YaRN: extrapolation mix factor (default: 1.0, 0.0 = full interpolation)
  --yarn-attn-factor N  YaRN: scale sqrt(t) or attention magnitude (default: 1.0)
  --yarn-beta-slow N    YaRN: high correction dim or alpha (default: 1.0)
  --yarn-beta-fast N    YaRN: low correction dim or beta (default: 32.0)
  --ignore-eos          ignore end of stream token and continue generating (implies --logit-bias 2-inf)
  --no-penalize-nl      do not penalize newline token
  --temp N              temperature (default: 0.8)
  --logits-all          return logits for all tokens in the batch (default: disabled)
  --hellaswag           compute HellaSwag score over random tasks from datafile supplied with -f
  --hellaswag-tasks N   number of tasks to use when computing the HellaSwag score (default: 400)
  --keep N              number of tokens to keep from the initial prompt (default: 0, -1 = all)
  --draft N             number of tokens to draft for speculative decoding (default: 8)
  --chunks N            max number of chunks to process (default: -1, -1 = all)
  -np N, --parallel N   number of parallel sequences to decode (default: 1)
  -ns N, --sequences N  number of sequences to decode (default: 1)
  -pa N, --p-accept N   speculative decoding accept probability (default: 0.5)
  -ps N, --p-split N    speculative decoding split probability (default: 0.1)
  -cb, --cont-batching  enable continuous batching (a.k.a dynamic batching) (default: disabled)
  --mmproj MMPROJ_FILE  path to a multimodal projector file for LLaVA. see examples/llava/README.md
  --image IMAGE_FILE    path to an image file. use with multimodal models
  --mlock               force system to keep model in RAM rather than swapping or compressing
  --no-mmap             do not memory-map model (slower load but may reduce pageouts if not using mlock)
  --numa                attempt optimizations that help on some NUMA systems
                        if run without this previously, it is recommended to drop the system page cache before using this
                        see https://github.com/ggerganov/llama.cpp/issues/1437
  --verbose-prompt      print prompt before generation
  -dkvc, --dump-kv-cache
                        verbose print of the KV cache
  -nkvo, --no-kv-offload
                        disable KV offload
  -ctk TYPE, --cache-type-k TYPE
                        KV cache data type for K (default: f16)
  -ctv TYPE, --cache-type-v TYPE
                        KV cache data type for V (default: f16)
  --simple-io           use basic IO for better compatibility in subprocesses and limited consoles
  --lora FNAME          apply LoRA adapter (implies --no-mmap)
  --lora-scaled FNAME S apply LoRA adapter with user defined scaling S (implies --no-mmap)
  --lora-base FNAME     optional model to use as a base for the layers modified by the LoRA adapter
  -m FNAME, --model FNAME
                        model path (default: models/7B/ggml-model-f16.gguf)
  -md FNAME, --model-draft FNAME
                        draft model for speculative decoding
  -ld LOGDIR, --logdir LOGDIR
                        path under which to save YAML logs (no logging if unset)
  --override-kv KEY=TYPE:VALUE
                        advanced option to override model metadata by key. may be specified multiple times.
                        types: int, float, bool. example: --override-kv tokenizer.ggml.add_bos_token=bool:false

log options:
  --log-test            Run simple logging test
  --log-disable         Disable trace logs
  --log-enable          Enable trace logs
  --log-file            Specify a log filename (without extension)
  --log-new             Create a separate new log file on start. Each log file will have unique name: "<name>.<ID>.log"
  --log-append          Don't truncate the old log file.

example interaction with ChatGPT 3.5 to produce a Lean proof

In a new conversation I provided the following prompt:

prompt

Answer the question based on the context below. Let's work this out in a step by step way to be sure we have the right answer.

Context: Lean is a proof assistant and programming language. Lean is based on the calculus of constructions with inductive types.

Context: There are multiple versions of Lean. This question is about Lean 4

`a=b` is a proposition. The variable `a` is Real valued and `b` is Real valued. Prove in version 4 of Lean that `(a=b) -> (a+2=b+2)`

ChatGTP 3.5 wrote in response

ChatGPT 3.5 response

Certainly! To prove the statement `(a = b) -> (a + 2 = b + 2)` in version 4 of Lean, you can follow these steps:

1. **Introduction of Variables**: Begin by introducing the variables and assumptions using the `variables` keyword. In this case, you have the variables `a` and `b` both being Real valued.

```lean
variables {a b : ℝ}

```

2. **Assumption**: State the assumption that `(a = b)`.

```lean
example (h : a = b) : a + 2 = b + 2 :=

```

3. **Transformation**: Use the assumption to transform the left-hand side of the conclusion `(a + 2)` to `(b + 2)` using the property of equality.

```lean
calc
   a + 2 = b + 2 : by rw h

```

Here, `calc` is used to chain together a sequence of expressions, and `rw h` applies the assumption `h`.

4. **QED (Quod Erat Demonstrandum)**: Conclude the proof.

```lean
   example (h : a = b) : a + 2 = b + 2 :=
   begin
     calc
       a + 2 = b + 2 : by rw h
   end

```

This step-by-step approach uses the Lean proof style to demonstrate the validity of the given proposition. The `calc` tactic is particularly useful for chaining together equalities.

On my computer I created a file "second_chatGPT_attempt.lean" and wrote

variables {a b : ℝ}

example (h : a = b) : a + 2 = b + 2 :=
begin
  calc
    a + 2 = b + 2 : by rw h
end

and then ran

docker run -it --rm -v `pwd`:/scratch --workdir /scratch lean3onubuntu lean --run second_chatGPT_attempt.lean
second_chatGPT_attempt.lean:2:0: error: unexpected identifier; expected command
second_chatGPT_attempt.lean:5:0: error: unknown identifier 'begin'
second_chatGPT_attempt.lean:6:2: error: unexpected token 'calc'; expected command
second_chatGPT_attempt.lean:8:0: error: invalid 'end', insufficient scopes

I then told ChatGPT

prompt

When I run the script

```lean
variables {a b : ℝ}

example (h : a = b) : a + 2 = b + 2 :=
begin
  calc
    a + 2 = b + 2 : by rw h
end

```

Lean 4 returns an error message: `error: unexpected identifier; expected command`

What should I do to fix the error?

ChatGPT 3.5 response

Apologies for the oversight. It seems I made an error in my previous responses. In Lean, you should use `theorem` or `example` as part of the proof declaration. Here's the corrected version:

```lean
variables {a b : ℝ}

theorem add_two_eq_add_two (h : a = b) : a + 2 = b + 2 :=
begin
  calc
    a + 2 = b + 2 : by rw h
end

```

In this corrected version, I replaced `example` with `theorem`. You can use `example` as well, but `theorem` is more appropriate when proving statements. This should resolve the error you encountered.

I then created a second Lean script, third_chatGPT_attempt.lean, and wrote

variables {a b : ℝ}

theorem add_two_eq_add_two (h : a = b) : a + 2 = b + 2 :=
begin
  calc
    a + 2 = b + 2 : by rw h
end

which got the same error as before when I attempted to run the script using Lean 4:

docker run -it --rm -v `pwd`:/scratch --workdir /scratch lean3onubuntu lean --run third_chatGPT_attempt.lean 
third_chatGPT_attempt.lean:1:0: error: unexpected identifier; expected command
third_chatGPT_attempt.lean:4:0: error: unknown identifier 'begin'
third_chatGPT_attempt.lean:5:2: error: unexpected token 'calc'; expected command
third_chatGPT_attempt.lean:7:0: error: invalid 'end', insufficient scopes
  

LLM prompts for the Physics Derivation Graph

Posing a prompt that gets a useful result currently requires some consideration. Below are some possible tasks for LLMs, along with additional context for the LLM.

Convert Latex to SymPy

TODO:

• Provide context for Latex - https://en.wikipedia.org/wiki/LaTeX
• Provide context for SymPy - https://en.wikipedia.org/wiki/SymPy
• Provide example conversions 
• before submitting the prompt to an LLM, make sure the Latex is valid - https://quicklatex.com/

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: SymPy is an open-source Python library for symbolic computation. SymPy provides a computer algebra system. SymPy can convert Latex math to SymPy, and SymPy can render a mathematical expression as Latex.

Question: What is the SymPy representation for the Latex expression $x^2 + y^2 = 1$ ?

Answer:

Right response:

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: SymPy is an open-source Python library for symbolic computation. SymPy provides a computer algebra system. SymPy can convert Latex math to SymPy, and SymPy can render a mathematical expression as Latex.

Question: What is the SymPy representation for the Latex expression $\vec{p}_{electron} = \vec{p}_{1}-\vec{p}_{2}$ ?

Answer:

Right response:

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: SymPy is an open-source Python library for symbolic computation. SymPy provides a computer algebra system. SymPy can convert Latex math to SymPy, and SymPy can render a mathematical expression as Latex.

Question: What is the SymPy representation for the Latex expression $x = \langle\psi_{\alpha}| \hat{A} |\psi_{\beta}\rangle$ ?

Answer:

Right response:

Specify the mathematical relation between period and frequency as an equation in Latex

TODO:

• define period
• define frequency - https://en.wikipedia.org/wiki/Frequency
• Provide context for Latex - https://en.wikipedia.org/wiki/LaTeX
• provide example 

Caveat: the page https://en.wikipedia.org/wiki/Frequency includes the statement that

"period is the reciprocal of the frequency: f = 1/T."

Use the context below to produce a result. Keep the response short and concise. Respond "Unsure about answer" if not sure about the answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: Period (symbol T) is the interval of time between events. Frequency (symbol f) is the number of occurrences of a repeating event per unit of time

Specify the mathematical relation between period and frequency as an equation in Latex.

Find arxiv papers with derivations

TODO:

• Explain arxiv
• define what I mean by a derivation
• Provide example citations

Provide citations based on the context below. 

Context: arxiv is an open-access repository of electronic preprints

Context: a derivation in mathematical Physics consists of a sequence of steps. Each step relates mathematical expressions to an inference rule. An expression is comprised of symbols and operators. An inference rule typically transforms input expressions into output expressions.

Cite three papers from arxiv that contain mathematical derivations with more than four steps.

Identify derivation steps between physics equations

TODO:

• define what I mean by a derivation
• Provide example steps

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer. Let's work this out in a step by step way to be sure we have the right answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: a derivation in mathematical Physics consists of a sequence of steps. Each step relates mathematical expressions to an inference rule. An expression is comprised of symbols and operators. An inference rule typically transforms input expressions into output expressions.

Question: What mathematical steps relate the Latex math expression $i x = log(y)$ and $\exp(i x) = y$ ?

Answer:

Right answer: Raise both sides as the power of $\exp$

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer. Let's work this out in a step by step way to be sure we have the right answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: a derivation in mathematical Physics consists of a sequence of steps. Each step relates mathematical expressions to an inference rule. An expression is comprised of symbols and operators. An inference rule typically transforms input expressions into output expressions.

Question: What is the derivative of $y = \cos(x) + i \sin(x)$ with respect to $x$ ?

Answer:

Right answer: $\frac{d}{dx} y = -\sin(x) + i\cos(x)$

Derive the wave function for a quantum particle in a 1D box

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer. Let's work this out in a step by step way to be sure we have the right answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: a derivation in mathematical Physics consists of a sequence of steps. Each step relates mathematical expressions to an inference rule. An expression is comprised of symbols and operators. An inference rule typically transforms input expressions into output expressions.

Question: derive the wave function for a quantum particle in a 1D box

Answer:

Right answer: see https://derivationmap.net/review_derivation/000010/

Derive Newton's Law of Universal Gravitation

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer. Let's work this out in a step by step way to be sure we have the right answer.

Context: a derivation in mathematical Physics consists of a sequence of steps. Each step relates mathematical expressions to an inference rule. An expression is comprised of symbols and operators. An inference rule typically transforms input expressions into output expressions.

provide a derivation of Newton's Law of Universal Gravitation

See https://physicsderivationgraph.blogspot.com/2023/06/finding-derivations-of-newtons-law-of.html

Convert derivation steps to a proof in Lean

TODO:

• define what I mean by a derivation
• Explain lean
• Provide example
• Emphasize correctness and precision

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer. Let's work this out in a step by step way to be sure we have the right answer.

Context: Lean is a proof assistant and programming language. Lean is based on the calculus of constructions with inductive types.

`a=b` is a proposition. The variable `a` is Real valued and `b` is Real valued. Prove in Lean that `(a=b) -> (a+2=b+2)`

Identify symbols in latex arxiv papers

TODO:

• Provide example
• Emphasize correctness and precision

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Question: What mathematical expressions are present in the following Latex?

```
\begin{equation}
a = b + c
\end{equation}
Assuming you know $b$, then
\begin{equation}
b*c = f
\end{equation}
```

Answer:

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Question: What variables are present in the following Latex?

```
\begin{equation}
a = b + c
\end{equation}
Assuming you know $b$, then
\begin{equation}
b*c = f
\end{equation}
```

Answer: