Instantly share code, notes, and snippets.

🎯
Focusing

# Brando Miranda brando90

🎯
Focusing
Created May 9, 2024 21:55
helm_prompt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 # -- 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 Created May 9, 2024 21:31 minerva_prompt_cot.py This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters  # -- 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: Last active May 9, 2024 05:11 initial_reprover_in_pypentrograph.py This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters  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.""" 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 ---- 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 Created April 6, 2024 01:28 kavity.bib This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters  @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} Created March 2, 2024 23:50 reciprocal_has_unbounded_limit.lean This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters  /- 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 Created March 2, 2024 20:52 vertical_asymptote_of_1_over_x.lean This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters  /- -/ 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] Created March 2, 2024 20:51 readme_main_repo.md This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters  **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 Created March 2, 2024 20:50 install_learning_lean.sh This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters  # -- 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
Created March 2, 2024 20:49
.gitignore
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 # Byte-compiled / optimized / DLL files __pycache__/ *.py[cod] *\$py.class # C extensions *.so # Distribution / packaging .Python