Skip to content

Instantly share code, notes, and snippets.

# -- HELM prompt, 8 shot, CoT? ref: https://storage.googleapis.com/crfm-helm-public/lite/benchmark_output/runs/v1.0.0/math:subject=algebra,level=1,use_official_examples=False,use_chain_of_thought=True,model=01-ai_yi-34b/scenario_state.json, https://crfm.stanford.edu/helm/lite/latest/#/runs/math:subject=algebra,level=1,use_official_examples=False,use_chain_of_thought=True,model=01-ai_yi-34b
HELM_MATH_PROMPT: str = (
"""Given a mathematics problem, determine the answer. Simplify your answer as much as possible.###
Problem: Let $r=3^s-s$ and $s=2^n+1$. What is the value of $r$ when $n=2$?
Answer: First substitute $n=2$ into the expression for $s$ to find $s=2^2+1=5$. Then substitute $s=5$ into the expression for $r$ to find $r=3^5-5=243-5=\\boxed{238}.###
Problem: If $x^{2y}= 4$ and $x = 4$, what is the value of $y$? Express your answer as a common fraction.
Answer: Plugging $x = 4$ into the first equation, we get $4^{2y} = 4^1 \\Rightarrow 2y = 1 \\Rightarrow y = \\boxed{\\frac{1}{2}}.###
Problem: If $y = \\dis
@brando90
brando90 / minerva_prompt_cot.py
Created May 9, 2024 21:31
minerva_prompt_cot.py
# -- Prompt minerva MATH 3 - better minerva + cot/scratch_pad
# https://github.com/EleutherAI/lm-evaluation-harness/blob/main/lm_eval/tasks/minerva_math/utils.py#L22
H_MATH_MINERVA_PROMPT_TEMPLATE_3_COT = (
r"""Problem:
Find the domain of the expression $\frac{\sqrt{x-2}}{\sqrt{5-x}}$.}
Solution:
Let's think step by step. The expressions inside each square root must be non-negative. Therefore, $x-2 \ge 0$, so $x\ge2$, and $5 - x \ge 0$, so $x \le 5$. Also, the denominator cannot be equal to zero, so $5-x>0$, which gives $x<5$. Therefore, the domain of the expression is $\boxed{[2,5)}$.
Problem:
@brando90
brando90 / gist:769e71f376b4a9a78ad63c6989be6a52
Last active May 9, 2024 05:11
initial_reprover_in_pypentrograph.py
import math
from pantograph.server import Server, ServerError
from pantograph.expr import GoalState, TacticHave, TacticCalc, Tactic
from loguru import logger
from dataclasses import dataclass, field
from typing import Optional, List, Tuple
@dataclass(frozen=True)
class SearchResult:
"""The result of attempting to prove a theorem."""
@brando90
brando90 / vectoring_lowering_uncertainty_research_planning.md
Created April 25, 2024 17:45
vectoring_lowering_uncertainty_research_planning.md

---- Prompts for Assessing & Rubber Ducking discussions on your research plan according to Vectoring ----

references: - https://web.stanford.edu/class/cs197/slides/04-vectoring.pdf

We should have three prompts. One tackling a different way to mitigate risks and uncertainties in projects with uncertainties -- especially in computer science and machine learning research. They are:

  • Prompt 1: attempting to guess/extrapolate/identifying unknown unknowns -- to reduce risks we are unaware of.
  • Prompt 2: asses my vectoring plan with assumptions for effective tackling of the unknown i.e., research
@inproceedings{langley00,
author = {P. Langley},
title = {Crafting Papers on Machine Learning},
year = {2000},
pages = {1207--1216},
editor = {Pat Langley},
booktitle = {Proceedings of the 17th International Conference
on Machine Learning (ICML 2000)},
address = {Stanford, CA},
publisher = {Morgan Kaufmann}
@brando90
brando90 / gist:0323f9e2a659580978ec5daa72f41333
Created March 2, 2024 23:50
reciprocal_has_unbounded_limit.lean
/-
theorem: lim_{x -> c+} f(x) = +infinity
x + infinit = +infinity
lim_{x -> c} f(x) = L
∀ ε > 0, ∃ δ > 0, 0 < |x - c| < δ → 0 < |f(x) - L| < ε
L = + infinity
consider some ε > 0
@brando90
brando90 / gist:0786c13414a510d4652351a2d96b51fc
Created March 2, 2024 20:52
vertical_asymptote_of_1_over_x.lean
/-
-/
import Mathlib.Data.Real.Basic
-- define 1/x (reciprical) for reals
noncomputable def f (x : ℝ ): ℝ := x⁻¹
#check f
-- unit test that f 1 = 1, f 2 = 1/2
theorem test_f1 : f 1 = 1 := by simp[f]
**Do not** run `install.sh` blindly.
There is no guarantee it will work on your machine.
Therefore, understand each command and only run the next command if the current one succeeded.
## For developing Lean in this repo
If you git cloned this repo with say `git clone git@github.com:brando90/learning_lean.git` then you will have the lean project `lean_src_proj` folder and it won't have it's Lean depedencies e.g., Mathlib or the `.lake` folder will be missing.
If that is the case, then you need to install mathlib for this project (note doing `lake +leanprover/lean4:nightly-2023-02-04 new my_project math` as suggested by the Lean [projects setup will fail](https://leanprover-community.github.io/install/project.html#creating-a-lean-project) does **not work**) with:
```bash
# -- Setup our lean_src_proj project for the first time (ref: https://leanprover-community.github.io/install/project.html#lean-projects)
# - Go to a folder where you want to create a project in a subfolder lean_src, and type lake +leanprover/lean4:nightly-2023-02-04 new lean_src math
# go to root of project (not the lean project)
cd $HOME/learning_lean
# Option1: set up the main lean_src_proj project for the first time:
# lake +leanprover/lean4:nightly-2023-02-04 new lean_src_proj math
# Option 2: set up main lean_src_proj project if you did a git clone of root learning_lean (so depedencies, e.g., matblib need to be installed)
# mkdir lean_src_proj
# cd lean_src_proj
# lake update
# Byte-compiled / optimized / DLL files
__pycache__/
*.py[cod]
*$py.class
# C extensions
*.so
# Distribution / packaging
.Python