brando90

```
conda install -c conda-forge opam 

...

This path already exists in the target prefix, and it won't be removed
by an uninstall action in this transaction. The path is one that conda
doesn't recognize. It may have been created by another package manager.

brando90

context: https://stackoverflow.com/questions/74695464/why-cant-i-install-ruby-3-1-2-in-linux?noredirect=1#comment131843536_74695464

```
$ ruby-build --definitions
1.8.5-p52
1.8.5-p113
1.8.5-p114
1.8.5-p115
1.8.5-p231
1.8.6

brando90

#!/usr/bin/env bash

# -- apt isn't recommended, always see official install isntructions
#RUN apt-get install -y --no-install-recommends rbenv
#RUN apt-get install -y --no-install-recommends ruby-build
#RUN apt-get install -y --no-install-recommends ruby-full
#RUN rbenv install 3.1.2
#RUN rbenv global 3.1.2

# -- apt isn't recommended, always see official install isntructions

brando90

"""
Decision, chunk data up to having 4096 tokens which is approximately 3072 words which is approximately 16,896 chars. Then llama2's training/tokenizer can truncate to a max length i.e. 4096 if it's too long. 
(To avoid losing some context at the boundaries, we will include 50 chars from the end of previous sequence.)
https://chat.openai.com/c/d64d19cf-1261-44c9-bfa0-3472d327138e

refs:
- https://chat.openai.com/share/cec64728-9c40-4ce5-acb1-042019c1eb61
- https://claude.ai/chat/634c2a5f-675a-400b-9256-79e69cc02c6d
- https://huggingface.co/mafmaticians
"""

brando90

kinit brando9@CS.STANFORD.EDU

ssh brando9@login.sherlock.stanford.edu
ssh brando9@skampere1.stanford.edu


CS 197
/afs/ir/class/cs197

https://docs.google.com/document/d/1A3StDOlJCRBD4CSd44FSj_JxqnWhW7hbEjXqkJKFuvk/edit 

brando90

-- https://leanprover-community.github.io/lean-web-editor/#code=--%20Skipping%20importing%20default%20nat%20libraries%0A--%20import%20data.nat.basic%20--%20imports%20standard%20nats%20in%20lean%0A%0A----%201.%20Defining%20unary%20natural%20numbers%20%28could%20have%20defined%20it%20as%20my_nat%29%0Ainductive%20u_nat%20%3A%20Type%0A%7C%20zero%20%3A%20u_nat%20--%20%230%0A%7C%20succ%20%3A%20u_nat%20%E2%86%92%20u_nat%20--%20%231%0A--%20Open%20the%20namespace%20to%20use%20%60zero%60%20and%20%60succ%60%20without%20prefix.%20So%20you%20don't%20have%20to%20do%20unary_nat.zero%20or%20unary_nat.succ%0Aopen%20u_nat%0A%0A----%202.%20let's%20construct%20some%20natural%20numbers!%0A%23eval%20zero%0A--%20%23reduce%20zero%0A%23eval%20succ%20zero%0A--%20%23reduce%20succ%20zero%0A%23eval%20succ%28succ%20zero%29%0A--%20%23reduce%20succ%28succ%20zero%29%0A%0A------%203.%20Let's%20define%20addition%20recursively%20%28on%20the%20right%29%0Adef%20add%20%3A%20u_nat%20%E2%86%92%20u_nat%20%E2%86%92%20u_nat%20%0A--%20def%20add%20%28n%2

brando90

Simplified version of Dually Ground BackTranslation for AutoFormalization:

def train_to_af_for_maf(mdl : causal_lm,
                        formal_data_set, # e.g., ITP lib like mathlib
                        informal_data_set,  # e.g., time-tested maths textbook e.g., Rudin, CLRS.
                        ):
    for (nl, fl*) in formal_data_set; for (nl*, fl) in informal_data_set;
        # -- Learn to Formalize: nl_i->fl* from fl* -> [nl_i]_i -> fl*
        [nl_i]_i := mdl("informalize " + fl*, sampling=top_p, num_out=k)  # noise is good for robustness!

brando90

# -- make vscode workspace
# decided not to have name of repo cuz I'd need to have conda env + github repo match name for making things simpler
cd /afs/cs.stanford.edu/u/brando9/
vscode_file="vscode.gold-ai-olympiad.afs_snap.code-workspace"
echo $vscode_file
touch $vscode_file
echo '{
    "folders": [
        {
            "path": "gold-ai-olympiad"

brando90

/-

-/
inductive UnaryNat : Type
| zero : UnaryNat
| succ : UnaryNat → UnaryNat
deriving Repr

#check UnaryNat
#check UnaryNat.zero

brando90

Hi Lean Provers! Curious, I know that https://leanprover-community.github.io/mathlib4_docs/ is good for referencing the mathlib docs. If I want to see all of the main Lean4 syntax/constructs e.g., building types, strucs, functions, what is the recommended website? Similarly is there a cheat sheet/table for this?
1 reply


Jibiana Jakpor
  22 minutes ago
Functional Programming in Lean is a great resource for learning the syntax, especially for general purpose programming: https://leanprover.github.io/functional_programming_in_lean/. It doesn’t have much info on tactics though. That’s where MIL or Theorem Proving in Lean 4 will serve you bette


# Learning to write Lean