From 0e5a7dc4a757b4f38dd9635a39455cef805829da Mon Sep 17 00:00:00 2001 From: Sai Konkimalla Date: Thu, 30 May 2024 12:34:16 -0700 Subject: [PATCH 1/3] Added proof_search.py based on llemma_formal2formal proof search method --- pantograph/proof_search.py | 579 +++++++++++++++++++++++++++++++++++++ 1 file changed, 579 insertions(+) create mode 100644 pantograph/proof_search.py diff --git a/pantograph/proof_search.py b/pantograph/proof_search.py new file mode 100644 index 0000000..af8654d --- /dev/null +++ b/pantograph/proof_search.py @@ -0,0 +1,579 @@ +""" +Class which uses a Pantograph instance to aid proof search. All calls to the kernel uses this +interface. +""" +from pantograph.expr import Variable, Goal, GoalState, \ + Tactic, TacticHave, TacticCalc + +from pantograph.server import Server, ServerError + +import os +import json +import heapq +import time +import random + +from datetime import datetime +from pathlib import Path +from tqdm import tqdm, trange +from openai import OpenAI + +# temporarily comment out (not directly using LLM through vllm) +# import transformers +# import vllm + +os.environ['TOKENIZERS_PARALLELISM'] = 'false' + +def generate_vllm(prompt, model, tokenizer, temperatures, num_samples, stop, max_tokens=256): + """ + Function for enabling vllm-based model to generate tactics for proof search + """ + texts, scores = [], [] + for temperature in temperatures: + params = vllm.SamplingParams( + n=num_samples, + temperature=temperature, + use_beam_search=temperature==0.0, + max_tokens=max_tokens, + stop=stop, + ) + outputs = model.generate([prompt], params, use_tqdm=False) + if len(outputs) == 0: + return [], [] + for output in outputs[0].outputs: + text = output.text.replace(tokenizer.eos_token, '') + score = output.cumulative_logprob/max(len(output.token_ids), 1) + texts.append(text) + scores.append(score) + + texts, scores = _unique_sorted(texts, scores) + return texts, scores + +def generate_llm_test(prompt, model, tokenizer, temperatures, num_samples, stop, max_tokens=256): + """ + Function for testing BFS proof search algorithm manually (by inputting next tactic) + """ + texts, scores = [], [] + for temperature in temperatures: + new_prompt = "Using a temperature of " + str(temperature) + " and with max tokens of " + str(max_tokens) + ", answer the following question:\n" + prompt + + print("\033[2J\033[H", end="", flush=True) + print(new_prompt) + + text = input("\nOutput: ") + score = -random.random() + + texts.append(text) + scores.append(score) + + texts, scores = _unique_sorted(texts, scores) + return texts, scores + +def generate_llm_openai_model(prompt, client, model_name, temperatures, num_samples, stop, max_tokens=256): + """ + Function for enabling OpenAI LLM model to generate tactics for proof search + """ + texts, scores = [], [] + for temperature in temperatures: + + completion = client.chat.completions.create( + model=model_name, + messages=[ + {"role": "user", "content": prompt} + ], + max_tokens=max_tokens, + temperature=temperature, + n=num_samples, + stop=stop, + logprobs=True + ) + + for i in range(num_samples): + choice = completion.choices[i] + + text = "" + score = 0.0 + token_count = 0 + + lp_content = choice.logprobs.content + + for token_lp in lp_content: + score -= token_lp.logprob + token_count += 1 + token = token_lp.token + + # strip generated message to only look at first tactic generated (ignore everything after , or ; or \n) + if ";" in token: + text += token_lp.token[:token.index(";")] + break + elif "," in token: + text += token_lp.token[:token.index(",")] + break + elif "\n" in token: + text += token_lp.token[:token.index("\n")] + break + else: + text += token + + token_count = max(token_count, 1) + score /= token_count + + texts.append(text) + scores.append(score) + + texts, scores = _unique_sorted(texts, scores) + return texts, scores + +def _unique_sorted(texts, scores): + texts_ = [] + scores_ = [] + for t, s in sorted(zip(texts, scores), key=lambda x: -x[1]): + if t not in texts_: + texts_.append(t) + scores_.append(s) + return texts_, scores_ + +def _tactic_state(state): + if isinstance(state, GoalState): + ts = "\n".join([str(goal).strip() for goal in state.goals]) + else: + ts = state + return ts + +def _prompt_oneshot(ts): + prompt = """Given the Lean 4 tactic state, suggest a next tactic. +Here is an example: + +Tactic state: +--- +m n : ℕ +h : Nat.coprime m n +⊢ Nat.gcd m n = 1 +--- +Next tactic: +--- +rw [← h.gcd_eq_one] +--- + +Tactic state: +--- +%s +--- +Next tactic: +---""" % (ts) + return prompt + +def _prompt_fewshot(ts): + prompt = """Given the Lean 4 tactic state, suggest a next tactic. +Here are some examples: + +Tactic state: +--- +α : Type u_1 +r : α → α → Prop +inst✝¹ : DecidableEq α +inst✝ : IsIrrefl α r +⊢ CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ fun x x_1 => x ≠ x_1) fun x x_1 => x < x_1) ↑toFinsupp +--- +Next tactic: +--- +rintro s t ⟨u, a, hr, he⟩ +--- + +Tactic state: +--- +ι : Type u_1 +I✝ J✝ : Box ι +x y : ι → ℝ +I J : WithBot (Box ι) +⊢ ↑I = ↑J ↔ I = J +--- +Next tactic: +--- +simp only [Subset.antisymm_iff, ← le_antisymm_iff, withBotCoe_subset_iff] +--- + +Tactic state: +--- +m n : ℕ +h : Nat.coprime m n +⊢ Nat.gcd m n = 1 +--- +Next tactic: +--- +rw [← h.gcd_eq_one] +--- + +Tactic state: +--- +%s +--- +Next tactic: +---""" % (ts) + return prompt + +def best_first_search( + server, + theorem, + theorem_name, + theorem_num, + client, + model_name, + max_iters, + temperatures, + num_samples, + prompt_fn, + timeout, + log_dir, + early_stop=False, + max_tokens=256 +) -> dict: + """Best first search.""" + attempt_results = [] + f = open(log_dir + "/" + theorem_name + ".txt", "a") + + f.write("Theorem number: " + str(theorem_count)) + + try: + init_state = server.goal_start(theorem) + + f.write("\n\nInitial state:\n") + f.write(_tactic_state(init_state).strip()) + + start = time.time() + proof_finished = False + queue = [(0.0, [], init_state, [])] + visited = set() + + for iteration in trange(max_iters): + # print("Iteration number: " + str(iteration+1)) + + f.write("\n\n---------------------------") + f.write("\nIteration " + str(iteration+1)) + f.write("\n---------------------------\n") + + if len(queue) == 0 or proof_finished: + break + + total_score, steps, state, trace = heapq.heappop(queue) + goal = state.goals[0] + ts = _tactic_state(state) + visited.add(ts) + + step_cands, step_scores = generate_llm_openai_model( + prompt_fn(ts), + client, + model_name, + temperatures, + num_samples, + stop='---', + max_tokens=max_tokens + ) + + step_cands = [s.strip() for s in step_cands] + + f.write("\nTactic candidates:\n") + f.write(str(step_cands)) + f.write("\n\nTactic scores (-log prob):\n") + f.write(str(step_scores)) + + # print(step_cands) + # print(step_scores) + # input() + + step_count = 1 + + for step, score in zip(step_cands, step_scores): + result = server.goal_tactic(state, 0, step) + step_trace = { + "tactic": step, + "state_before": ts + } + + rs = _tactic_state(result) + solved = "solved" if result.is_solved else "not solved" + + f.write("\n\nTactic " + str(step_count) + " result: " + solved + "\n") + f.write(rs) + + # print(result) + # print(result.is_solved) + # input() + + if result.is_solved: + elapsed_time = time.time() - start + + attempt_results.append({ + 'theorem': theorem, + 'proof': steps + [step], + 'score': total_score - score, + 'success': True, + 'failure_reason': '', + 'trace': trace + [step_trace], + 'temperature': temperatures, + 'elapsed': elapsed_time, + 'iteration': iteration + }) + if early_stop: + return attempt_results + proof_finished = True + + f.write("\n\nTheorem proven!") + f.write("\nElapsed time: " + str(elapsed_time)) + break + else: + if _tactic_state(result) not in visited: + # Score is negative log probability summed across steps + new_score = (total_score + score) + heapq.heappush( + queue, (new_score, steps+[step], result, trace+[step_trace]) + ) + + except ServerError as e: + # print(e) + # print(str(e)) + + if len(attempt_results) == 0: + attempt_results.append({ + 'theorem': theorem, + 'success': False, + 'failure_reason': type(e).__name__ + }) + + f.write("\n\nTheorem error") + f.write("\nFailure reason: " + str(type(e).__name__) + " " + str(e)) + + if len(attempt_results) == 0: + attempt_results.append({ + 'theorem': theorem, + 'success': False, + 'failure_reason': 'SearchEnded' + }) + + f.write("\Theorem not proven") + f.write("Failure reason: SearchEnded") + + f.close() + + return attempt_results + +def _save(model_name, results, args_dict, output_dir, shard): + Path(output_dir).mkdir(parents=True, exist_ok=True) + output_file = os.path.join( + output_dir, + 'results__%s__%s.json' % (model_name.replace('/', '_'), shard) + ) + with open(output_file, 'w') as f: + json.dump({ + 'results': results, + 'args': args_dict + }, f, indent=4) + print(output_file) + +def _load_model(model_name, tp_degree): + """ + Old function to load model using vllm + """ + model = vllm.LLM( + model=model_name, + tensor_parallel_size=tp_degree, + dtype='bfloat16', + max_num_batched_tokens=4096 + ) + tokenizer = transformers.AutoTokenizer.from_pretrained(model_name) + return model, tokenizer + +def _load_client(api_key): + """ + New function to load client using OpenAI API + """ + client = OpenAI( + api_key=api_key + ) + return client + +def _load_data(dataset_name, dataset_path): + """ + Old function to load dataset from minif2f dataset + """ + if 'minif2f' in dataset_name: + data = [] + with open(dataset_path) as f: + for line in f.readlines(): + data_ = json.loads(line) + assert data_['commit'] == 'd00c776260c77de7e70125ef0cd119de6c0ff1de' + data.append(data_) + + if 'valid' in dataset_name: + data = [x for x in data if x['split'] == 'valid'] + else: + data = [x for x in data if x['split'] == 'test'] + # repo = LeanGitRepo(data[0]['url'], data[0]['commit']) + repo = None + else: + raise NotImplementedError(dataset_name) + + return repo, data + +def _load_data2(dataset_name, dataset_path): + """ + New function load dataset from test dataset (only meant to check functionality of proof search) + """ + data = [] + with open(dataset_path) as f: + for line in f.readlines(): + data_ = json.loads(line) + data.append(data_) + + return data + +def _get_api_key(path): + """ + Function to get OpenAI API key stored externally (would be normally stored in the program in another method) + """ + key_file = open(path, 'r') + key = key_file.readlines()[0] + key_file.close() + return key + +def print_stats(results): + print(len([x for x in results if x['success']]) / len(results)) + print("# successes: ", len([x for x in results if x['success']]), sep="\t") + +def resume_from(results_filename, data): + results = json.load(open(results_filename))['results'] + data = data[len(results):] + print("=== Resuming from %d" % (len(results))) + return results, data + +def make_output_dir(output_dir): + dt = datetime.now().strftime("%d-%m-%Y-%H-%M") + output_dir = os.path.join(output_dir, dt) + Path(output_dir).mkdir(parents=True, exist_ok=True) + + log_dir = os.path.join(output_dir, "logs") + Path(log_dir).mkdir(parents=True, exist_ok=True) + return output_dir, log_dir + +def pause(): + """ + Infinite while loop for debugging purposes + """ + while True: + x = 1 + +if __name__ == '__main__': + import argparse + + parser = argparse.ArgumentParser() + parser.add_argument( + '--model-name', + choices=[ + 'open-web-math/llemma_7b', + 'open-web-math/llemma_34b', + 'codellama/CodeLlama-7b-hf', + 'codellama/CodeLlama-34b-hf', + 'gpt-3.5-turbo', + 'gpt-4' + ], + default='gpt-3.5-turbo' + ) + parser.add_argument( + '--dataset-name', + choices=['minif2f-valid', 'minif2f-test', 'test-set'], + default='test-set' + ) + parser.add_argument('--shard', type=int, default=0) + parser.add_argument('--resume-from', type=str, default=None) + parser.add_argument( + '--dataset-path', + choices=['data/minif2f.jsonl', 'data/test.jsonl'], + default='data/test.jsonl' + ) + parser.add_argument('--output-dir', default='output/test') + parser.add_argument('--early-stop', action='store_true') + parser.add_argument('--tp-degree', type=int, default=1) + parser.add_argument('--num-shards', type=int, default=8) + parser.add_argument('--max-iters', type=int, default=5) + parser.add_argument('--timeout', type=int, default=600) + parser.add_argument('--num-examples', type=int, default=-1) + parser.add_argument('--num-samples', type=int, default=1) + parser.add_argument('--clear-process-hours', type=int, default=3) + parser.add_argument('--temperatures', type=float, nargs='+', default=[0.0]) + parser.add_argument('--api-key-path', type=str, default='../api_key/key.txt') + args = parser.parse_args() + + key = _get_api_key(args.api_key_path) + client = _load_client(key) + model_name = args.model_name + + output_dir, log_dir = make_output_dir(args.output_dir) + + repo = None + data = None + shard_size = None + + if (args.dataset_name == 'test-set'): + data = _load_data2(args.dataset_name, args.dataset_path) + else: + repo, data = _load_data(args.dataset_name, args.dataset_path) + shard_size = len(data) // args.num_shards + data = data[args.shard*shard_size:(args.shard+1)*shard_size] + print("Shard size: %d" % (len(data))) + + if args.resume_from is not None: + results, data = resume_from(args.resume_from, data) + else: + results = [] + + start = time.time() + server = Server() + + theorem_count = 1 + + for example in tqdm(data, total=len(data)): + + file_path = example['file_path'] + theorem_name = example['full_name'] + theorem = example['statement'] + + attempt_results = best_first_search( + server=server, + theorem=theorem, + theorem_name=theorem_name, + theorem_num=theorem_count, + client=client, + model_name=model_name, + max_iters=args.max_iters, + temperatures=args.temperatures, + num_samples=args.num_samples, + prompt_fn=_prompt_oneshot, + timeout=args.timeout, + log_dir=log_dir, + early_stop=args.early_stop + ) + result = { + 'attempt_results': attempt_results, + 'success': any([x['success'] for x in attempt_results]), + 'example': example + } + results.append(result) + + theorem_count += 1 + + _save( + model_name=args.model_name, + results=results, + args_dict=args.__dict__, + output_dir=output_dir, + shard=args.shard + ) + print_stats(results) + # The proof search occasionally leaves Lean processes open. As a workaround, + # we periodically kill all Lean processes. Note that this may cause a proof search failure. + if args.shard == 0: + hours = 60*60*args.clear_process_hours + if time.time() - start > hours: + print("=== Killing active leanprover processes to mitigate leak") + os.system("ps aux | grep leanprover | awk '{print $2}' | xargs kill -9") + start = time.time() \ No newline at end of file From f4ec1a8730e9d3c39a5edc51ace8b6afca420850 Mon Sep 17 00:00:00 2001 From: Sai Konkimalla Date: Thu, 30 May 2024 12:45:31 -0700 Subject: [PATCH 2/3] Added respective datasets used in testing proof search function --- data/minif2f.jsonl | 488 +++++++++++++++++++++++++++++++++++++++++++++ data/test.jsonl | 2 + 2 files changed, 490 insertions(+) create mode 100644 data/minif2f.jsonl create mode 100644 data/test.jsonl diff --git a/data/minif2f.jsonl b/data/minif2f.jsonl new file mode 100644 index 0000000..fe24512 --- /dev/null +++ b/data/minif2f.jsonl @@ -0,0 +1,488 @@ +{"full_name": "amc12a_2019_p21", "statement": "theorem amc12a_2019_p21 (z : \u2102) (h\u2080 : z = (1 + Complex.I) / Real.sqrt 2) :\n ((\u2211 k : \u2124 in Finset.Icc 1 12, z ^ k ^ 2) * (\u2211 k : \u2124 in Finset.Icc 1 12, 1 / z ^ k ^ 2)) = 36", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2015_p10", "statement": "theorem amc12a_2015_p10 (x y : \u2124) (h\u2080 : 0 < y) (h\u2081 : y < x) (h\u2082 : x + y + x * y = 80) : x = 26", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2008_p8", "statement": "theorem amc12a_2008_p8 (x y : \u211d) (h\u2080 : 0 < x \u2227 0 < y) (h\u2081 : y ^ 3 = 1)\n (h\u2082 : 6 * x ^ 2 = 2 * (6 * y ^ 2)) : x ^ 3 = 2 * Real.sqrt 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_182", "statement": "theorem mathd_algebra_182 (y : \u2102) : 7 * (3 * y + 2) = 21 * y + 14", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aime_1984_p5", "statement": "theorem aime_1984_p5 (a b : \u211d) (h\u2080 : Real.logb 8 a + Real.logb 4 (b ^ 2) = 5)\n (h\u2081 : Real.logb 8 b + Real.logb 4 (a ^ 2) = 7) : a * b = 512", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_780", "statement": "theorem mathd_numbertheory_780 (m x : \u2115) (h\u2080 : 10 \u2264 m) (h\u2081 : m \u2264 99) (h\u2082 : 6 * x % m = 1)\n (h\u2083 : (x - 6 ^ 2) % m = 0) : m = 43", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_116", "statement": "theorem mathd_algebra_116 (k x : \u211d) (h\u2080 : x = (13 - Real.sqrt 131) / 4)\n (h\u2081 : 2 * x ^ 2 - 13 * x + k = 0) : k = 19 / 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_13", "statement": "theorem mathd_numbertheory_13 (u v : \u2115) (S : Set \u2115)\n (h\u2080 : \u2200 n : \u2115, n \u2208 S \u2194 0 < n \u2227 14 * n % 100 = 46) (h\u2081 : IsLeast S u)\n (h\u2082 : IsLeast (S \\ {u}) v) : (u + v : \u211a) / 2 = 64", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_169", "statement": "theorem mathd_numbertheory_169 : Nat.gcd 20! 200000 = 40000", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2009_p9", "statement": "theorem amc12a_2009_p9 (a b c : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f (x + 3) = 3 * x ^ 2 + 7 * x + 4)\n (h\u2081 : \u2200 x, f x = a * x ^ 2 + b * x + c) : a + b + c = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2019_p9", "statement": "theorem amc12a_2019_p9 (a : \u2115 \u2192 \u211a) (h\u2080 : a 1 = 1) (h\u2081 : a 2 = 3 / 7)\n (h\u2082 : \u2200 n, a (n + 2) = a n * a (n + 1) / (2 * a n - a (n + 1))) :\n \u2191(a 2019).den + (a 2019).num = 8078", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_13", "statement": "theorem mathd_algebra_13 (a b : \u211d)\n (h\u2080 : \u2200 x, x - 3 \u2260 0 \u2227 x - 5 \u2260 0 \u2192 4 * x / (x ^ 2 - 8 * x + 15) = a / (x - 3) + b / (x - 5)) :\n a = -6 \u2227 b = 10", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "induction_sum2kp1npqsqm1", "statement": "theorem induction_sum2kp1npqsqm1 (n : \u2115) :\n (\u2211 k in Finset.range n, 2 * k + 3) = (n + 1) ^ 2 - 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aime_1991_p6", "statement": "theorem aime_1991_p6 (r : \u211d) (h\u2080 : (\u2211 k in Finset.Icc (19 : \u2115) 91, Int.floor (r + k / 100)) = 546) :\n Int.floor (100 * r) = 743", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_149", "statement": "theorem mathd_numbertheory_149 :\n (\u2211 k in Finset.filter (fun x => x % 8 = 5 \u2227 x % 6 = 3) (Finset.range 50), k) = 66", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1984_p2", "statement": "theorem imo_1984_p2 (a b : \u2115) (h\u2080 : 0 < a \u2227 0 < b) (h\u2081 : \u00ac7 \u2223 a) (h\u2082 : \u00ac7 \u2223 b) (h\u2083 : \u00ac7 \u2223 a + b)\n (h\u2084 : 7 ^ 7 \u2223 (a + b) ^ 7 - a ^ 7 - b ^ 7) : 19 \u2264 a + b", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2008_p4", "statement": "theorem amc12a_2008_p4 : (\u220f k in Finset.Icc (1 : \u2115) 501, ((4 : \u211d) * k + 4) / (4 * k)) = 502", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_2006_p6", "statement": "theorem imo_2006_p6 (a b c : \u211d) :\n a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2) \u2264\n 9 * Real.sqrt 2 / 32 * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_462", "statement": "theorem mathd_algebra_462 : ((1 : \u211a) / 2 + 1 / 3) * (1 / 2 - 1 / 3) = 5 / 36", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1964_p1_2", "statement": "theorem imo_1964_p1_2 (n : \u2115) : \u00ac7 \u2223 2 ^ n + 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_221", "statement": "theorem mathd_numbertheory_221 (S : Finset \u2115)\n (h\u2080 : \u2200 x : \u2115, x \u2208 S \u2194 0 < x \u2227 x < 1000 \u2227 x.divisors.card = 3) : S.card = 11", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_64", "statement": "theorem mathd_numbertheory_64 : IsLeast { x : \u2115 | 30 * x \u2261 42 [MOD 47] } 39", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1987_p4", "statement": "theorem imo_1987_p4 (f : \u2115 \u2192 \u2115) : \u2203 n, f (f n) \u2260 n + 1987", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_33", "statement": "theorem mathd_numbertheory_33 (n : \u2115) (h\u2080 : n < 398) (h\u2081 : n * 7 % 398 = 1) : n = 57", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12_2001_p9", "statement": "theorem amc12_2001_p9 (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x > 0, \u2200 y > 0, f (x * y) = f x / y) (h\u2081 : f 500 = 3) :\n f 600 = 5 / 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1965_p1", "statement": "theorem imo_1965_p1 (x : \u211d) (h\u2080 : 0 \u2264 x) (h\u2081 : x \u2264 2 * \u03c0)\n (h\u2082 :\n 2 * Real.cos x \u2264 abs (Real.sqrt (1 + Real.sin (2 * x)) - Real.sqrt (1 - Real.sin (2 * x))))\n (h\u2083 : abs (Real.sqrt (1 + Real.sin (2 * x)) - Real.sqrt (1 - Real.sin (2 * x))) \u2264 Real.sqrt 2) :\n \u03c0 / 4 \u2264 x \u2227 x \u2264 7 * \u03c0 / 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_48", "statement": "theorem mathd_numbertheory_48 (b : \u2115) (h\u2080 : 0 < b) (h\u2081 : 3 * b ^ 2 + 2 * b + 1 = 57) : b = 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "numbertheory_sqmod4in01d", "statement": "theorem numbertheory_sqmod4in01d (a : \u2124) : a ^ 2 % 4 = 0 \u2228 a ^ 2 % 4 = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_466", "statement": "theorem mathd_numbertheory_466 : (\u2211 k in Finset.range 11, k) % 9 = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_48", "statement": "theorem mathd_algebra_48 (q e : \u2102) (h\u2080 : q = 9 - 4 * Complex.I) (h\u2081 : e = -3 - 4 * Complex.I) :\n q - e = 12", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12_2000_p15", "statement": "theorem amc12_2000_p15 (f : \u2102 \u2192 \u2102) (h\u2080 : \u2200 x, f (x / 3) = x ^ 2 + x + 1)\n (h\u2081 : Fintype (f \u207b\u00b9' {7})) : (\u2211 y in (f \u207b\u00b9' {7}).toFinset, y / 3) = -1 / 9", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_132", "statement": "theorem mathd_numbertheory_132 : 2004 % 12 = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2009_p5", "statement": "theorem amc12a_2009_p5 (x : \u211d) (h\u2080 : x ^ 3 - (x + 1) * (x - 1) * x = 5) : x ^ 3 = 125", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_188", "statement": "theorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_224", "statement": "theorem mathd_algebra_224 (S : Finset \u2115)\n (h\u2080 : \u2200 n : \u2115, n \u2208 S \u2194 Real.sqrt n < 7 / 2 \u2227 2 < Real.sqrt n) : S.card = 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "induction_divisibility_3divnto3m2n", "statement": "theorem induction_divisibility_3divnto3m2n (n : \u2115) : 3 \u2223 n ^ 3 + 2 * n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "induction_sum_1oktkp1", "statement": "theorem induction_sum_1oktkp1 (n : \u2115) :\n (\u2211 k in Finset.range n, (1 : \u211d) / ((k + 1) * (k + 2))) = n / (n + 1)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_32", "statement": "theorem mathd_numbertheory_32 (S : Finset \u2115) (h\u2080 : \u2200 n : \u2115, n \u2208 S \u2194 n \u2223 36) : (\u2211 k in S, k) = 91", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_422", "statement": "theorem mathd_algebra_422 (x : \u211d) (\u03c3 : Equiv \u211d \u211d) (h\u2080 : \u2200 x, \u03c3.1 x = 5 * x - 12)\n (h\u2081 : \u03c3.1 (x + 1) = \u03c3.2 x) : x = 47 / 24", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12b_2002_p11", "statement": "theorem amc12b_2002_p11 (a b : \u2115) (h\u2080 : Nat.Prime a) (h\u2081 : Nat.Prime b) (h\u2082 : Nat.Prime (a + b))\n (h\u2083 : Nat.Prime (a - b)) : Nat.Prime (a + b + (a - b + (a + b)))", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_73", "statement": "theorem mathd_algebra_73 (p q r x : \u2102) (h\u2080 : (x - p) * (x - q) = (r - p) * (r - q)) (h\u2081 : x \u2260 r) :\n x = p + q - r", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_109", "statement": "theorem mathd_numbertheory_109 (v : \u2115 \u2192 \u2115) (h\u2080 : \u2200 n, v n = 2 * n - 1) :\n (\u2211 k in Finset.Icc 1 100, v k) % 7 = 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_xmysqpymzsqpzmxsqeqxyz_xpypzp6dvdx3y3z3", "statement": "theorem algebra_xmysqpymzsqpzmxsqeqxyz_xpypzp6dvdx3y3z3 (x y z : \u2124)\n (h\u2080 : (x - y) ^ 2 + (y - z) ^ 2 + (z - x) ^ 2 = x * y * z) :\n x + y + z + 6 \u2223 x ^ 3 + y ^ 3 + z ^ 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1962_p4", "statement": "theorem imo_1962_p4 (S : Set \u211d)\n (h\u2080 : S = { x : \u211d | Real.cos x ^ 2 + Real.cos (2 * x) ^ 2 + Real.cos (3 * x) ^ 2 = 1 }) :\n S =\n { x : \u211d |\n \u2203 m : \u2124,\n x = \u03c0 / 2 + m * \u03c0 \u2228\n x = \u03c0 / 4 + m * \u03c0 / 2 \u2228 x = \u03c0 / 6 + m * \u03c0 / 6 \u2228 x = 5 * \u03c0 / 6 + m * \u03c0 / 6 }", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_236", "statement": "theorem mathd_numbertheory_236 : 1999 ^ 2000 % 5 = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_24", "statement": "theorem mathd_numbertheory_24 : (\u2211 k in Finset.Icc 1 9, 11 ^ k) % 100 = 59", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_amgm_prod1toneq1_sum1tongeqn", "statement": "theorem algebra_amgm_prod1toneq1_sum1tongeqn (a : \u2115 \u2192 NNReal) (n : \u2115)\n (h\u2080 : Finset.prod (Finset.range n) a = 1) : Finset.sum (Finset.range n) a \u2265 n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_101", "statement": "theorem mathd_algebra_101 (x : \u211d) (h\u2080 : x ^ 2 - 5 * x - 4 \u2264 10) : x \u2265 -2 \u2227 x \u2264 7", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_257", "statement": "theorem mathd_numbertheory_257 (x : \u2115) (h\u2080 : 1 \u2264 x \u2227 x \u2264 100)\n (h\u2081 : 77 \u2223 (\u2211 k in Finset.range 101, k) - x) : x = 45", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12_2000_p5", "statement": "theorem amc12_2000_p5 (x p : \u211d) (h\u2080 : x < 2) (h\u2081 : abs (x - 2) = p) : x - p = 2 - 2 * p", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_547", "statement": "theorem mathd_algebra_547 (x y : \u211d) (h\u2080 : x = 5) (h\u2081 : y = 2) : Real.sqrt (x ^ 3 - 2 ^ y) = 11", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_200", "statement": "theorem mathd_numbertheory_200 : 139 % 11 = 7", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_510", "statement": "theorem mathd_algebra_510 (x y : \u211d) (h\u2080 : x + y = 13) (h\u2081 : x * y = 24) :\n Real.sqrt (x ^ 2 + y ^ 2) = 11", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_140", "statement": "theorem mathd_algebra_140 (a b c : \u211d) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c)\n (h\u2081 : \u2200 x, 24 * x ^ 2 - 19 * x - 35 = (a * x - 5) * (2 * (b * x) + c)) : a * b - 3 * c = -9", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_455", "statement": "theorem mathd_algebra_455 (x : \u211d) (h\u2080 : 2 * (2 * (2 * (2 * x))) = 48) : x = 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_45", "statement": "theorem mathd_numbertheory_45 : Nat.gcd 6432 132 + 11 = 23", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aime_1994_p4", "statement": "theorem aime_1994_p4 (n : \u2115) (h\u2080 : 0 < n)\n (h\u2080 : (\u2211 k in Finset.Icc 1 n, Int.floor (Real.logb 2 k)) = 1994) : n = 312", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_739", "statement": "theorem mathd_numbertheory_739 : 9! % 10 = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_245", "statement": "theorem mathd_algebra_245 (x : \u211d) (h\u2080 : x \u2260 0) :\n (4 / x)\u207b\u00b9 * (3 * x ^ 3 / x) ^ 2 * (1 / (2 * x))\u207b\u00b9 ^ 3 = 18 * x ^ 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_apb4leq8ta4pb4", "statement": "theorem algebra_apb4leq8ta4pb4 (a b : \u211d) (h\u2080 : 0 < a \u2227 0 < b) : (a + b) ^ 4 \u2264 8 * (a ^ 4 + b ^ 4)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_28", "statement": "theorem mathd_algebra_28 (c : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = 2 * x ^ 2 + 5 * x + c)\n (h\u2081 : \u2203 x, f x \u2264 0) : c \u2264 25 / 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_543", "statement": "theorem mathd_numbertheory_543 : (\u2211 k in Nat.divisors (30 ^ 4), 1) - 2 = 123", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_480", "statement": "theorem mathd_algebra_480 (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x < 0, f x = -x ^ 2 - 1)\n (h\u2081 : \u2200 x, 0 \u2264 x \u2227 x < 4 \u2192 f x = 2) (h\u2082 : \u2200 x \u2265 4, f x = Real.sqrt x) : f \u03c0 = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_69", "statement": "theorem mathd_algebra_69 (rows seats : \u2115) (h\u2080 : rows * seats = 450)\n (h\u2081 : (rows + 5) * (seats - 3) = 450) : rows = 25", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_433", "statement": "theorem mathd_algebra_433 (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = 3 * Real.sqrt (2 * x - 7) - 8) : f 8 = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_126", "statement": "theorem mathd_algebra_126 (x y : \u211d) (h\u2080 : 2 * 3 = x - 9) (h\u2081 : 2 * -5 = y + 1) : x = 15 \u2227 y = -11", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aimeII_2020_p6", "statement": "theorem aimeII_2020_p6 (t : \u2115 \u2192 \u211a) (h\u2080 : t 1 = 20) (h\u2081 : t 2 = 21)\n (h\u2082 : \u2200 n \u2265 3, t n = (5 * t (n - 1) + 1) / (25 * t (n - 2))) :\n \u2191(t 2020).den + (t 2020).num = 626", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2008_p2", "statement": "theorem amc12a_2008_p2 (x : \u211d) (h\u2080 : x * (1 / 2 + 2 / 3) = 1) : x = 6 / 7", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_35", "statement": "theorem mathd_algebra_35 (p q : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, p x = 2 - x ^ 2)\n (h\u2081 : \u2200 (x) (_ : x \u2260 0), q x = 6 / x) : p (q 2) = -7", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_amgm_faxinrrp2msqrt2geq2mxm1div2x", "statement": "theorem algebra_amgm_faxinrrp2msqrt2geq2mxm1div2x :\n \u2200 x > 0, 2 - Real.sqrt 2 \u2265 2 - x - 1 / (2 * x)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_335", "statement": "theorem mathd_numbertheory_335 (n : \u2115) (h\u2080 : n % 7 = 5) : 5 * n % 7 = 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_35", "statement": "theorem mathd_numbertheory_35 (S : Finset \u2115) (h\u2080 : \u2200 n : \u2115, n \u2223 Nat.sqrt 196) :\n (\u2211 k in S, k) = 24", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2021_p7", "statement": "theorem amc12a_2021_p7 (x y : \u211d) : 1 \u2264 (x * y - 1) ^ 2 + (x + y) ^ 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_327", "statement": "theorem mathd_algebra_327 (a : \u211d) (h\u2080 : 1 / 5 * abs (9 + 2 * a) < 1) : -7 < a \u2227 a < -2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aime_1984_p15", "statement": "theorem aime_1984_p15 (x y z w : \u211d)\n (h\u2080 :\n x ^ 2 / (2 ^ 2 - 1) + y ^ 2 / (2 ^ 2 - 3 ^ 2) + z ^ 2 / (2 ^ 2 - 5 ^ 2) +\n w ^ 2 / (2 ^ 2 - 7 ^ 2) =\n 1)\n (h\u2081 :\n x ^ 2 / (4 ^ 2 - 1) + y ^ 2 / (4 ^ 2 - 3 ^ 2) + z ^ 2 / (4 ^ 2 - 5 ^ 2) +\n w ^ 2 / (4 ^ 2 - 7 ^ 2) =\n 1)\n (h\u2082 :\n x ^ 2 / (6 ^ 2 - 1) + y ^ 2 / (6 ^ 2 - 3 ^ 2) + z ^ 2 / (6 ^ 2 - 5 ^ 2) +\n w ^ 2 / (6 ^ 2 - 7 ^ 2) =\n 1)\n (h\u2083 :\n x ^ 2 / (8 ^ 2 - 1) + y ^ 2 / (8 ^ 2 - 3 ^ 2) + z ^ 2 / (8 ^ 2 - 5 ^ 2) +\n w ^ 2 / (8 ^ 2 - 7 ^ 2) =\n 1) :\n x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2 = 36", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_amgm_sqrtxymulxmyeqxpy_xpygeq4", "statement": "theorem algebra_amgm_sqrtxymulxmyeqxpy_xpygeq4 (x y : \u211d) (h\u2080 : 0 < x \u2227 0 < y) (h\u2081 : y \u2264 x)\n (h\u2082 : Real.sqrt (x * y) * (x - y) = x + y) : x + y \u2265 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2002_p21", "statement": "theorem amc12a_2002_p21 (u : \u2115 \u2192 \u2115) (h\u2080 : u 0 = 4) (h\u2081 : u 1 = 7)\n (h\u2082 : \u2200 n \u2265 2, u (n + 2) = (u n + u (n + 1)) % 10) :\n \u2200 n, (\u2211 k in Finset.range n, u k) > 10000 \u2192 1999 \u2264 n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_192", "statement": "theorem mathd_algebra_192 (q e d : \u2102) (h\u2080 : q = 11 - 5 * Complex.I) (h\u2081 : e = 11 + 5 * Complex.I)\n (h\u2082 : d = 2 * Complex.I) : q * e * d = 292 * Complex.I", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12b_2002_p6", "statement": "theorem amc12b_2002_p6 (a b : \u211d) (h\u2080 : a \u2260 0 \u2227 b \u2260 0)\n (h\u2081 : \u2200 x, x ^ 2 + a * x + b = (x - a) * (x - b)) : a = 1 \u2227 b = -2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_102", "statement": "theorem mathd_numbertheory_102 : 2 ^ 8 % 5 = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2010_p22", "statement": "theorem amc12a_2010_p22 (x : \u211d) : 49 \u2264 \u2211 k:\u2124 in Finset.Icc 1 119, abs (\u2191k * x - 1)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_81", "statement": "theorem mathd_numbertheory_81 : 71 % 3 = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_155", "statement": "theorem mathd_numbertheory_155 :\n Finset.card (Finset.filter (fun x => x % 19 = 7) (Finset.Icc 100 999)) = 48", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1978_p5", "statement": "theorem imo_1978_p5 (n : \u2115) (a : \u2115 \u2192 \u2115) (h\u2080 : Function.Injective a) (h\u2081 : a 0 = 0) (h\u2082 : 0 < n) :\n (\u2211 k in Finset.Icc 1 n, (1 : \u211d) / k) \u2264 \u2211 k in Finset.Icc 1 n, a k / k ^ 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2017_p7", "statement": "theorem amc12a_2017_p7 (f : \u2115 \u2192 \u211d) (h\u2080 : f 1 = 2) (h\u2081 : \u2200 n, 1 < n \u2227 Even n \u2192 f n = f (n - 1) + 1)\n (h\u2082 : \u2200 n, 1 < n \u2227 Odd n \u2192 f n = f (n - 2) + 2) : f 2017 = 2018", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_42", "statement": "theorem mathd_numbertheory_42 (S : Set \u2115) (u v : \u2115) (h\u2080 : \u2200 a : \u2115, a \u2208 S \u2194 0 < a \u2227 27 * a % 40 = 17)\n (h\u2081 : IsLeast S u) (h\u2082 : IsLeast (S \\ {u}) v) : u + v = 62", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_110", "statement": "theorem mathd_algebra_110 (q e : \u2102) (h\u2080 : q = 2 - 2 * Complex.I) (h\u2081 : e = 5 + 5 * Complex.I) :\n q * e = 20", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12b_2021_p21", "statement": "theorem amc12b_2021_p21 (S : Finset \u211d)\n (h\u2080 : \u2200 x : \u211d, x \u2208 S \u2194 0 < x \u2227 x ^ (2 : \u211d) ^ Real.sqrt 2 = Real.sqrt 2 ^ (2 : \u211d) ^ x) :\n (\u21912 \u2264 \u2211 k in S, k) \u2227 (\u2211 k in S, k) < 6", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_405", "statement": "theorem mathd_algebra_405 (S : Finset \u2115) (h\u2080 : \u2200 x, x \u2208 S \u2194 0 < x \u2227 x ^ 2 + 4 * x + 4 < 20) :\n S.card = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "numbertheory_sumkmulnckeqnmul2pownm1", "statement": "theorem numbertheory_sumkmulnckeqnmul2pownm1 (n : \u2115) (h\u2080 : 0 < n) :\n (\u2211 k in Finset.Icc 1 n, k * Nat.choose n k) = n * 2 ^ (n - 1)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_393", "statement": "theorem mathd_algebra_393 (\u03c3 : Equiv \u211d \u211d) (h\u2080 : \u2200 x, \u03c3.1 x = 4 * x ^ 3 + 1) : \u03c3.2 33 = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12b_2004_p3", "statement": "theorem amc12b_2004_p3 (x y : \u2115) (h\u2080 : 2 ^ x * 3 ^ y = 1296) : x + y = 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_303", "statement": "theorem mathd_numbertheory_303 (S : Finset \u2115)\n (h\u2080 : \u2200 n : \u2115, n \u2208 S \u2194 2 \u2264 n \u2227 171 \u2261 80 [MOD n] \u2227 468 \u2261 13 [MOD n]) : (\u2211 k in S, k) = 111", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_151", "statement": "theorem mathd_algebra_151 : Int.ceil (Real.sqrt 27) - Int.floor (Real.sqrt 26) = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2011_p18", "statement": "theorem amc12a_2011_p18 (x y : \u211d) (h\u2080 : abs (x + y) + abs (x - y) = 2) :\n x ^ 2 - 6 * x + y ^ 2 \u2264 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_15", "statement": "theorem mathd_algebra_15 (s : \u2115 \u2192 \u2115 \u2192 \u2115)\n (h\u2080 : \u2200 a b, 0 < a \u2227 0 < b \u2192 s a b = a ^ (b : \u2115) + b ^ (a : \u2115)) : s 2 6 = 100", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_211", "statement": "theorem mathd_numbertheory_211 :\n Finset.card (Finset.filter (fun n => 6 \u2223 4 * \u2191n - (2 : \u2124)) (Finset.range 60)) = 20", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_640", "statement": "theorem mathd_numbertheory_640 : (91145 + 91146 + 91147 + 91148) % 4 = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12b_2003_p6", "statement": "theorem amc12b_2003_p6 (a r : \u211d) (u : \u2115 \u2192 \u211d) (h\u2080 : \u2200 k, u k = a * r ^ k) (h\u2081 : u 1 = 2)\n (h\u2082 : u 3 = 6) : u 0 = 2 / Real.sqrt 3 \u2228 u 0 = -(2 / Real.sqrt 3)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_2rootsintpoly_am10tap11eqasqpam110", "statement": "theorem algebra_2rootsintpoly_am10tap11eqasqpam110 (a : \u2102) :\n (a - 10) * (a + 11) = a ^ 2 + a - 110", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aime_1991_p1", "statement": "theorem aime_1991_p1 (x y : \u2115) (h\u2080 : 0 < x \u2227 0 < y) (h\u2081 : x * y + (x + y) = 71)\n (h\u2082 : x ^ 2 * y + x * y ^ 2 = 880) : x ^ 2 + y ^ 2 = 146", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_43", "statement": "theorem mathd_algebra_43 (a b : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = a * x + b) (h\u2081 : f 7 = 4)\n (h\u2082 : f 6 = 3) : f 3 = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1988_p6", "statement": "theorem imo_1988_p6 (a b : \u2115) (h\u2080 : 0 < a \u2227 0 < b) (h\u2081 : a * b + 1 \u2223 a ^ 2 + b ^ 2) :\n \u2203 x : \u2115, (x ^ 2 : \u211d) = (a ^ 2 + b ^ 2) / (a * b + 1)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aime_1996_p5", "statement": "theorem aime_1996_p5 (a b c r s t : \u211d) (f g : \u211d \u2192 \u211d)\n (h\u2080 : \u2200 x, f x = x ^ 3 + 3 * x ^ 2 + 4 * x - 11) (h\u2081 : \u2200 x, g x = x ^ 3 + r * x ^ 2 + s * x + t)\n (h\u2082 : f a = 0) (h\u2083 : f b = 0) (h\u2084 : f c = 0) (h\u2085 : g (a + b) = 0) (h\u2086 : g (b + c) = 0)\n (h\u2087 : g (c + a) = 0) (h\u2088 : List.Pairwise (\u00b7 \u2260 \u00b7) [a, b, c]) : t = 23", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_55", "statement": "theorem mathd_algebra_55 (q p : \u211d) (h\u2080 : q = 2 - 4 + 6 - 8 + 10 - 12 + 14)\n (h\u2081 : p = 3 - 6 + 9 - 12 + 15 - 18 + 21) : q / p = 2 / 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_sqineq_2at2pclta2c2p41pc", "statement": "theorem algebra_sqineq_2at2pclta2c2p41pc (a c : \u211d) :\n 2 * a * (2 + c) \u2264 a ^ 2 + c ^ 2 + 4 * (1 + c)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_43", "statement": "theorem mathd_numbertheory_43 : IsGreatest { n : \u2115 | 15 ^ n \u2223 942! } 233", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_214", "statement": "theorem mathd_algebra_214 (a : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = a * (x - 2) ^ 2 + 3) (h\u2081 : f 4 = 4) :\n f 6 = 7", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_96", "statement": "theorem mathd_algebra_96 (x y z a : \u211d) (h\u2080 : 0 < x \u2227 0 < y \u2227 0 < z)\n (h\u2081 : Real.log x - Real.log y = a) (h\u2082 : Real.log y - Real.log z = 15)\n (h\u2083 : Real.log z - Real.log x = -7) : a = -8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12_2001_p2", "statement": "theorem amc12_2001_p2 (a b n : \u2115) (h\u2080 : 1 \u2264 a \u2227 a \u2264 9) (h\u2081 : 0 \u2264 b \u2227 b \u2264 9) (h\u2082 : n = 10 * a + b)\n (h\u2083 : n = a * b + a + b) : b = 9", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_185", "statement": "theorem mathd_algebra_185 (s : Finset \u2124) (f : \u2124 \u2192 \u2124) (h\u2080 : \u2200 x, f x = abs (x + 4))\n (h\u2081 : \u2200 x, x \u2208 s \u2194 f x < 9) : s.card = 17", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_binomnegdiscrineq_10alt28asqp1", "statement": "theorem algebra_binomnegdiscrineq_10alt28asqp1 (a : \u211d) : 10 * a \u2264 28 * a ^ 2 + 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_284", "statement": "theorem mathd_numbertheory_284 (a b : \u2115) (h\u2080 : 1 \u2264 a \u2227 a \u2264 9 \u2227 b \u2264 9)\n (h\u2081 : 10 * a + b = 2 * (a + b)) : 10 * a + b = 18", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2009_p2", "statement": "theorem amc12a_2009_p2 : 1 + 1 / (1 + 1 / (1 + 1)) = (5 : \u211a) / 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_709", "statement": "theorem mathd_numbertheory_709 (n : \u2115) (h\u2080 : 0 < n) (h\u2081 : Finset.card (Nat.divisors (2 * n)) = 28)\n (h\u2082 : Finset.card (Nat.divisors (3 * n)) = 30) : Finset.card (Nat.divisors (6 * n)) = 35", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2013_p8", "statement": "theorem amc12a_2013_p8 (x y : \u211d) (h\u2080 : x \u2260 0) (h\u2081 : y \u2260 0) (h\u2082 : x \u2260 y)\n (h\u2083 : x + 2 / x = y + 2 / y) : x * y = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_461", "statement": "theorem mathd_numbertheory_461 (n : \u2115)\n (h\u2080 : n = Finset.card (Finset.filter (fun x => Nat.gcd x 8 = 1) (Finset.Icc 1 7))) :\n 3 ^ n % 8 = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_59", "statement": "theorem mathd_algebra_59 (b : \u211d) (h\u2080 : (4 : \u211d) ^ b + 2 ^ 3 = 12) : b = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_234", "statement": "theorem mathd_algebra_234 (d : \u211d) (h\u2080 : 27 / 125 * d = 9 / 25) : 3 / 5 * d ^ 3 = 25 / 9", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1973_p3", "statement": "theorem imo_1973_p3 (a b : \u211d) (h\u2080 : \u2203 x, x ^ 4 + a * x ^ 3 + b * x ^ 2 + a * x + 1 = 0) :\n 4 / 5 \u2264 a ^ 2 + b ^ 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12b_2020_p5", "statement": "theorem amc12b_2020_p5 (a b : \u2115) (h\u2080 : (5 : \u211a) / 8 * b = 2 / 3 * a + 7)\n (h\u2081 : (b : \u211a) - 5 / 8 * b = a - 2 / 3 * a + 7) : a = 42", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "numbertheory_sqmod3in01d", "statement": "theorem numbertheory_sqmod3in01d (a : \u2124) : a ^ 2 % 3 = 0 \u2228 a ^ 2 % 3 = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_131", "statement": "theorem mathd_algebra_131 (a b : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = 2 * x ^ 2 - 7 * x + 2)\n (h\u2081 : f a = 0) (h\u2082 : f b = 0) (h\u2083 : a \u2260 b) : 1 / (a - 1) + 1 / (b - 1) = -1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12b_2003_p17", "statement": "theorem amc12b_2003_p17 (x y : \u211d) (h\u2080 : 0 < x \u2227 0 < y) (h\u2081 : Real.log (x * y ^ 3) = 1)\n (h\u2082 : Real.log (x ^ 2 * y) = 1) : Real.log (x * y) = 3 / 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_536", "statement": "theorem mathd_algebra_536 : \u21913! * ((2 : \u211d) ^ 3 + Real.sqrt 9) / 2 = (33 : \u211d)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_22", "statement": "theorem mathd_algebra_22 : Real.logb (5 ^ 2) (5 ^ 4) = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "numbertheory_xsqpysqintdenomeq", "statement": "theorem numbertheory_xsqpysqintdenomeq (x y : \u211a) (h\u2080 : (x ^ 2 + y ^ 2).den = 1) : x.den = y.den", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aimeII_2001_p3", "statement": "theorem aimeII_2001_p3 (x : \u2115 \u2192 \u2124) (h\u2080 : x 1 = 211) (h\u2082 : x 2 = 375) (h\u2083 : x 3 = 420)\n (h\u2084 : x 4 = 523) (h\u2086 : \u2200 n \u2265 5, x n = x (n - 1) - x (n - 2) + x (n - 3) - x (n - 4)) :\n x 531 + x 753 + x 975 = 898", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_22", "statement": "theorem mathd_numbertheory_22 (b : \u2115) (h\u2080 : b < 10)\n (h\u2081 : Nat.sqrt (10 * b + 6) * Nat.sqrt (10 * b + 6) = 10 * b + 6) : b = 3 \u2228 b = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aime_1987_p8", "statement": "theorem aime_1987_p8 :\n IsGreatest { n : \u2115 | 0 < n \u2227 \u2203! k : \u2115, (8 : \u211d) / 15 < n / (n + k) \u2227 (n : \u211d) / (n + k) < 7 / 13 }\n 112", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_136", "statement": "theorem mathd_numbertheory_136 (n : \u2115) (h\u2080 : 123 * n + 17 = 39500) : n = 321", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12_2000_p11", "statement": "theorem amc12_2000_p11 (a b : \u211d) (h\u2080 : a \u2260 0 \u2227 b \u2260 0) (h\u2081 : a * b = a - b) :\n a / b + b / a - a * b = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12b_2003_p9", "statement": "theorem amc12b_2003_p9 (a b : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = a * x + b) (h\u2081 : f 6 - f 2 = 12) :\n f 12 - f 2 = 30", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_2complexrootspoly_xsqp49eqxp7itxpn7i", "statement": "theorem algebra_2complexrootspoly_xsqp49eqxp7itxpn7i (x : \u2102) :\n x ^ 2 + 49 = (x + 7 * Complex.I) * (x + -7 * Complex.I)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_198", "statement": "theorem mathd_numbertheory_198 : 5 ^ 2005 % 100 = 25", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_149", "statement": "theorem mathd_algebra_149 (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x < -5, f x = x ^ 2 + 5)\n (h\u2081 : \u2200 x \u2265 -5, f x = 3 * x - 8) (h\u2082 : Fintype (f \u207b\u00b9' {10})) :\n (\u2211 k in (f \u207b\u00b9' {10}).toFinset, k) = 6", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_132", "statement": "theorem mathd_algebra_132 (x : \u211d) (f g : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = x + 2) (h\u2081 : \u2200 x, g x = x ^ 2)\n (h\u2082 : f (g x) = g (f x)) : x = -1 / 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_37", "statement": "theorem mathd_numbertheory_37 : Nat.lcm 9999 100001 = 90900909", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aime_1983_p9", "statement": "theorem aime_1983_p9 (x : \u211d) (h\u2080 : 0 < x \u2227 x < Real.pi) :\n 12 \u2264 (9 * (x ^ 2 * Real.sin x ^ 2) + 4) / (x * Real.sin x)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_37", "statement": "theorem mathd_algebra_37 (x y : \u211d) (h\u2080 : x + y = 7) (h\u2081 : 3 * x + y = 45) : x ^ 2 - y ^ 2 = 217", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_458", "statement": "theorem mathd_numbertheory_458 (n : \u2115) (h\u2080 : n % 8 = 7) : n % 4 = 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2008_p15", "statement": "theorem amc12a_2008_p15 (k : \u2115) (h\u2080 : k = 2008 ^ 2 + 2 ^ 2008) : (k ^ 2 + 2 ^ k) % 10 = 6", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_301", "statement": "theorem mathd_numbertheory_301 (j : \u2115) (h\u2080 : 0 < j) : 3 * (7 * \u2191j + 3) % 7 = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2009_p15", "statement": "theorem amc12a_2009_p15 (n : \u2115) (h\u2080 : 0 < n)\n (h\u2081 : (\u2211 k in Finset.Icc 1 n, \u2191k * Complex.I ^ k) = 48 + 49 * Complex.I) : n = 97", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_sqineq_36azm9asqle36zsq", "statement": "theorem algebra_sqineq_36azm9asqle36zsq (z a : \u211d) : 36 * (a * z) - 9 * a ^ 2 \u2264 36 * z ^ 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2013_p7", "statement": "theorem amc12a_2013_p7 (s : \u2115 \u2192 \u211d) (h\u2080 : \u2200 n, s (n + 2) = s (n + 1) + s n) (h\u2081 : s 9 = 110)\n (h\u2082 : s 7 = 42) : s 4 = 10", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_104", "statement": "theorem mathd_algebra_104 (x : \u211d) (h\u2080 : 125 / 8 = x / 12) : x = 375 / 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_252", "statement": "theorem mathd_numbertheory_252 : 7! % 23 = 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2020_p21", "statement": "theorem amc12a_2020_p21 (S : Finset \u2115)\n (h\u2080 : \u2200 n : \u2115, n \u2208 S \u2194 5 \u2223 n \u2227 Nat.lcm 5! n = 5 * Nat.gcd 10! n) : S.card = 48", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_493", "statement": "theorem mathd_algebra_493 (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = x ^ 2 - 4 * Real.sqrt x + 1) :\n f (f 4) = 70", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "numbertheory_nckeqnm1ckpnm1ckm1", "statement": "theorem numbertheory_nckeqnm1ckpnm1ckm1 (n k : \u2115) (h\u2080 : 0 < n \u2227 0 < k) (h\u2081 : k \u2264 n) :\n Nat.choose n k = Nat.choose (n - 1) k + Nat.choose (n - 1) (k - 1)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_3rootspoly_amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta", "statement": "theorem algebra_3rootspoly_amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta (b c d a : \u2102) :\n (a - d) * (a - c) * (a - b) =\n -((a ^ 2 - (b + c) * a + c * b) * d) + (a ^ 2 - (b + c) * a + c * b) * a", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_403", "statement": "theorem mathd_numbertheory_403 : (\u2211 k in Nat.properDivisors 198, k) = 270", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_190", "statement": "theorem mathd_algebra_190 : ((3 : \u211d) / 8 + 7 / 8) / (4 / 5) = 25 / 16", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_269", "statement": "theorem mathd_numbertheory_269 : (2005 ^ 2 + 2005 ^ 0 + 2005 ^ 0 + 2005 ^ 5) % 100 = 52", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aime_1990_p2", "statement": "theorem aime_1990_p2 :\n (52 + 6 * Real.sqrt 43) ^ ((3 : \u211d) / 2) - (52 - 6 * Real.sqrt 43) ^ ((3 : \u211d) / 2) = 828", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_101", "statement": "theorem mathd_numbertheory_101 : 17 * 18 % 4 = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_sqineq_4bap1lt4bsqpap1sq", "statement": "theorem algebra_sqineq_4bap1lt4bsqpap1sq (a b : \u211d) : 4 * b * (a + 1) \u2264 4 * b ^ 2 + (a + 1) ^ 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_156", "statement": "theorem mathd_numbertheory_156 (n : \u2115) (h\u2080 : 0 < n) : Nat.gcd (n + 7) (2 * n + 1) \u2264 13", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_451", "statement": "theorem mathd_algebra_451 (\u03c3 : Equiv \u211d \u211d) (h\u2080 : \u03c3.2 (-15) = 0) (h\u2081 : \u03c3.2 0 = 3) (h\u2082 : \u03c3.2 3 = 9)\n (h\u2083 : \u03c3.2 9 = 20) : \u03c3.1 (\u03c3.1 9) = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_144", "statement": "theorem mathd_algebra_144 (a b c d : \u2115) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c \u2227 0 < d) (h\u2080 : (c : \u2124) - b = d)\n (h\u2081 : (b : \u2124) - a = d) (h\u2082 : a + b + c = 60) (h\u2083 : a + b > c) : d < 10", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_282", "statement": "theorem mathd_algebra_282 (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x : \u211d, \u00ac (Irrational x) \u2192 f x = abs (Int.floor x))\n (h\u2081 : \u2200 x, Irrational x \u2192 f x = (Int.ceil x) ^ 2) :\n f (8 ^ (1 / 3)) + f (-Real.pi) + f (Real.sqrt 50) + f (9 / 2) = 79", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_410", "statement": "theorem mathd_algebra_410 (x y : \u211d) (h\u2080 : y = x ^ 2 - 6 * x + 13) : 4 \u2264 y", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_232", "statement": "theorem mathd_numbertheory_232 (x y z : ZMod 31) (h\u2080 : x = 3\u207b\u00b9) (h\u2081 : y = 5\u207b\u00b9)\n (h\u2082 : z = (x + y)\u207b\u00b9) : z = 29", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_77", "statement": "theorem mathd_algebra_77 (a b : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : a \u2260 0 \u2227 b \u2260 0) (h\u2081 : a \u2260 b)\n (h\u2082 : \u2200 x, f x = x ^ 2 + a * x + b) (h\u2083 : f a = 0) (h\u2084 : f b = 0) : a = 1 \u2227 b = -2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1974_p5", "statement": "theorem imo_1974_p5 (a b c d s : \u211d) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c \u2227 0 < d)\n (h\u2081 : s = a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)) :\n 1 < s \u2227 s < 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aime_1988_p3", "statement": "theorem aime_1988_p3 (x : \u211d) (h\u2080 : 0 < x)\n (h\u2081 : Real.logb 2 (Real.logb 8 x) = Real.logb 8 (Real.logb 2 x)) : Real.logb 2 x ^ 2 = 27", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_530", "statement": "theorem mathd_numbertheory_530 (n k : \u2115) (h\u2080 : 0 < n \u2227 0 < k) (h\u2080 : (n : \u211d) / k < 6)\n (h\u2081 : (5 : \u211d) < n / k) : 22 \u2264 Nat.lcm n k / Nat.gcd n k", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_109", "statement": "theorem mathd_algebra_109 (a b : \u211d) (h\u2080 : 3 * a + 2 * b = 12) (h\u2081 : a = 4) : b = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1967_p3", "statement": "theorem imo_1967_p3 (k m n : \u2115) (c : \u2115 \u2192 \u2115) (h\u2080 : 0 < k \u2227 0 < m \u2227 0 < n)\n (h\u2081 : \u2200 s, c s = s * (s + 1)) (h\u2082 : Nat.Prime (k + m + 1)) (h\u2083 : n + 1 < k + m + 1) :\n (\u220f i in Finset.Icc 1 n, c i) \u2223 \u220f i in Finset.Icc 1 n, c (m + i) - c k", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_11", "statement": "theorem mathd_algebra_11 (a b : \u211d) (h\u2080 : a \u2260 b) (h\u2081 : a \u2260 2 * b)\n (h\u2082 : (4 * a + 3 * b) / (a - 2 * b) = 5) : (a + 11 * b) / (a - b) = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2003_p1", "statement": "theorem amc12a_2003_p1 (u v : \u2115 \u2192 \u2115) (h\u2080 : \u2200 n, u n = 2 * n + 2) (h\u2081 : \u2200 n, v n = 2 * n + 1) :\n ((\u2211 k in Finset.range 2003, u k) - \u2211 k in Finset.range 2003, v k) = 2003", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "numbertheory_aneqprodakp4_anmsqrtanp1eq2", "statement": "theorem numbertheory_aneqprodakp4_anmsqrtanp1eq2 (a : \u2115 \u2192 \u211d) (h\u2080 : a 0 = 1)\n (h\u2081 : \u2200 n, a (n + 1) = (\u220f k in Finset.range (n + 1), a k) + 4) :\n \u2200 n \u2265 1, a n - Real.sqrt (a (n + 1)) = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_2rootspoly_apatapbeq2asqp2ab", "statement": "theorem algebra_2rootspoly_apatapbeq2asqp2ab (a b : \u2102) :\n (a + a) * (a + b) = 2 * a ^ 2 + 2 * (a * b)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "induction_sum_odd", "statement": "theorem induction_sum_odd (n : \u2115) : (\u2211 k in Finset.range n, 2 * k) + 1 = n ^ 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_568", "statement": "theorem mathd_algebra_568 (a : \u211d) :\n (a - 1) * (a + 1) * (a + 2) - (a - 2) * (a + 1) = a ^ 3 + a ^ 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_616", "statement": "theorem mathd_algebra_616 (f g : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = x ^ 3 + 2 * x + 1)\n (h\u2081 : \u2200 x, g x = x - 1) : f (g 1) = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_690", "statement": "theorem mathd_numbertheory_690 :\n IsLeast { a : \u2115 | 0 < a \u2227 a \u2261 2 [MOD 3] \u2227 a \u2261 4 [MOD 5] \u2227 a \u2261 6 [MOD 7] \u2227 a \u2261 8 [MOD 9] } 314", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2016_p2", "statement": "theorem amc12a_2016_p2 (x : \u211d) (h\u2080 : (10 : \u211d) ^ x * 100 ^ (2 * x) = 1000 ^ 5) : x = 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_405", "statement": "theorem mathd_numbertheory_405 (a b c : \u2115) (t : \u2115 \u2192 \u2115) (h\u2080 : t 0 = 0) (h\u2081 : t 1 = 1)\n (h\u2082 : \u2200 n > 1, t n = t (n - 2) + t (n - 1)) (h\u2083 : a \u2261 5 [MOD 16]) (h\u2084 : b \u2261 10 [MOD 16])\n (h\u2085 : c \u2261 15 [MOD 16]) : (t a + t b + t c) % 7 = 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_110", "statement": "theorem mathd_numbertheory_110 (a b : \u2115) (h\u2080 : 0 < a \u2227 0 < b \u2227 b \u2264 a) (h\u2081 : (a + b) % 10 = 2)\n (h\u2082 : (2 * a + b) % 10 = 1) : (a - b) % 10 = 6", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2003_p25", "statement": "theorem amc12a_2003_p25 (a b : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : 0 < b)\n (h\u2081 : \u2200 x, f x = Real.sqrt (a * x ^ 2 + b * x)) (h\u2082 : { x | 0 \u2264 f x } = f '' { x | 0 \u2264 f x }) :\n a = 0 \u2228 a = -4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2010_p10", "statement": "theorem amc12a_2010_p10 (p q : \u211d) (a : \u2115 \u2192 \u211d) (h\u2080 : \u2200 n, a (n + 2) - a (n + 1) = a (n + 1) - a n)\n (h\u2081 : a 1 = p) (h\u2082 : a 2 = 9) (h\u2083 : a 3 = 3 * p - q) (h\u2084 : a 4 = 3 * p + q) : a 2010 = 8041", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_509", "statement": "theorem mathd_algebra_509 :\n Real.sqrt ((5 / Real.sqrt 80 + Real.sqrt 845 / 9 + Real.sqrt 45) / Real.sqrt 5) = 13 / 6", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_159", "statement": "theorem mathd_algebra_159 (b : \u211d) (f : \u211d \u2192 \u211d)\n (h\u2080 : \u2200 x, f x = 3 * x ^ 4 - 7 * x ^ 3 + 2 * x ^ 2 - b * x + 1) (h\u2081 : f 1 = 1) : b = -2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aime_1997_p11", "statement": "theorem aime_1997_p11 (x : \u211d)\n (h\u2080 :\n x =\n (\u2211 n in Finset.Icc (1 : \u2115) 44, Real.cos (n * \u03c0 / 180)) /\n \u2211 n in Finset.Icc (1 : \u2115) 44, Real.sin (n * \u03c0 / 180)) :\n Int.floor (100 * x) = 241", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aimeI_2000_p7", "statement": "theorem aimeI_2000_p7 (x y z : \u211d) (m : \u211a) (h\u2080 : 0 < x \u2227 0 < y \u2227 0 < z) (h\u2081 : x * y * z = 1)\n (h\u2082 : x + 1 / z = 5) (h\u2083 : y + 1 / x = 29) (h\u2084 : z + 1 / y = m) (h\u2085 : 0 < m) :\n \u2191m.den + m.num = 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "aime_1988_p4", "statement": "theorem aime_1988_p4 (n : \u2115) (a : \u2115 \u2192 \u211d) (h\u2080 : \u2200 n, abs (a n) < 1)\n (h\u2081 : (\u2211 k in Finset.range n, abs (a k)) = 19 + abs (\u2211 k in Finset.range n, a k)) : 20 \u2264 n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "induction_divisibility_9div10tonm1", "statement": "theorem induction_divisibility_9div10tonm1 (n : \u2115) (h\u2080 : 0 < n) : 9 \u2223 10 ^ n - 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_126", "statement": "theorem mathd_numbertheory_126 (x a : \u2115) (h\u2080 : 0 < x \u2227 0 < a) (h\u2081 : Nat.gcd a 40 = x + 3)\n (h\u2082 : Nat.lcm a 40 = x * (x + 3))\n (h\u2083 : \u2200 b : \u2115, 0 < b \u2192 Nat.gcd b 40 = x + 3 \u2227 Nat.lcm b 40 = x * (x + 3) \u2192 a \u2264 b) : a = 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_323", "statement": "theorem mathd_algebra_323 (\u03c3 : Equiv \u211d \u211d) (h : \u2200 x, \u03c3.1 x = x ^ 3 - 8) : \u03c3.2 (\u03c3.1 (\u03c3.2 19)) = 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_421", "statement": "theorem mathd_algebra_421 (a b c d : \u211d) (h\u2080 : b = a ^ 2 + 4 * a + 6)\n (h\u2081 : b = 1 / 2 * a ^ 2 + a + 6) (h\u2082 : d = c ^ 2 + 4 * c + 6) (h\u2083 : d = 1 / 2 * c ^ 2 + c + 6)\n (h\u2084 : a < c) : c - a = 6", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1987_p6", "statement": "theorem imo_1987_p6 (p : \u2115) (f : \u2115 \u2192 \u2115) (h\u2080 : \u2200 x, f x = x ^ 2 + x + p)\n (h\u2080 : \u2200 k : \u2115, k \u2264 Nat.floor (Real.sqrt (p / 3)) \u2192 Nat.Prime (f k)) :\n \u2200 i \u2264 p - 2, Nat.Prime (f i)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2009_p25", "statement": "theorem amc12a_2009_p25 (a : \u2115 \u2192 \u211d) (h\u2080 : a 1 = 1) (h\u2081 : a 2 = 1 / Real.sqrt 3)\n (h\u2082 : \u2200 n, 1 \u2264 n \u2192 a (n + 2) = (a n + a (n + 1)) / (1 - a n * a (n + 1))) : abs (a 2009) = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1961_p1", "statement": "theorem imo_1961_p1 (x y z a b : \u211d) (h\u2080 : 0 < x \u2227 0 < y \u2227 0 < z) (h\u2081 : x \u2260 y) (h\u2082 : y \u2260 z)\n (h\u2083 : z \u2260 x) (h\u2084 : x + y + z = a) (h\u2085 : x ^ 2 + y ^ 2 + z ^ 2 = b ^ 2) (h\u2086 : x * y = z ^ 2) :\n 0 < a \u2227 b ^ 2 < a ^ 2 \u2227 a ^ 2 < 3 * b ^ 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_31", "statement": "theorem mathd_algebra_31 (x : NNReal) (u : \u2115 \u2192 NNReal) (h\u2080 : \u2200 n, u (n + 1) = NNReal.sqrt (x + u n))\n (h\u2081 : Filter.Tendsto u Filter.atTop (\ud835\udcdd 9)) : 9 = NNReal.sqrt (x + 9)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_manipexpr_apbeq2cceqiacpbceqm2", "statement": "theorem algebra_manipexpr_apbeq2cceqiacpbceqm2 (a b c : \u2102) (h\u2080 : a + b = 2 * c)\n (h\u2081 : c = Complex.I) : a * c + b * c = -2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_370", "statement": "theorem mathd_numbertheory_370 (n : \u2115) (h\u2080 : n % 7 = 3) : (2 * n + 1) % 7 = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_437", "statement": "theorem mathd_algebra_437 (x y : \u211d) (n : \u2124) (h\u2080 : x ^ 3 = -45) (h\u2081 : y ^ 3 = -101) (h\u2082 : x < n)\n (h\u2083 : \u2191n < y) : n = -4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1966_p5", "statement": "theorem imo_1966_p5 (x a : \u2115 \u2192 \u211d) (h\u2080 : a 1 \u2260 a 2) (h\u2081 : a 1 \u2260 a 3) (h\u2082 : a 1 \u2260 a 4)\n (h\u2083 : a 2 \u2260 a 3) (h\u2084 : a 2 \u2260 a 4) (h\u2085 : a 3 \u2260 a 4) (h\u2086 : a 1 > a 2) (h\u2087 : a 2 > a 3)\n (h\u2088 : a 3 > a 4)\n (h\u2089 : abs (a 1 - a 2) * x 2 + abs (a 1 - a 3) * x 3 + abs (a 1 - a 4) * x 4 = 1)\n (h\u2081\u2080 : abs (a 2 - a 1) * x 1 + abs (a 2 - a 3) * x 3 + abs (a 2 - a 4) * x 4 = 1)\n (h\u2081\u2081 : abs (a 3 - a 1) * x 1 + abs (a 3 - a 2) * x 2 + abs (a 3 - a 4) * x 4 = 1)\n (h\u2081\u2082 : abs (a 4 - a 1) * x 1 + abs (a 4 - a 2) * x 2 + abs (a 4 - a 3) * x 3 = 1) :\n x 2 = 0 \u2227 x 3 = 0 \u2227 x 1 = 1 / abs (a 1 - a 4) \u2227 x 4 = 1 / abs (a 1 - a 4)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_89", "statement": "theorem mathd_algebra_89 (b : \u211d) (h\u2080 : b \u2260 0) :\n (7 * b ^ 3) ^ 2 * (4 * b ^ 2) ^ (-(3 : \u2124)) = 49 / 64", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1966_p4", "statement": "theorem imo_1966_p4 (n : \u2115) (x : \u211d) (h\u2080 : \u2200 k : \u2115, 0 < k \u2192 \u2200 m : \u2124, x \u2260 m * \u03c0 / 2 ^ k)\n (h\u2081 : 0 < n) :\n (\u2211 k in Finset.Icc 1 n, 1 / Real.sin (2 ^ k * x)) = 1 / Real.tan x - 1 / Real.tan (2 ^ n * x)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_67", "statement": "theorem mathd_algebra_67 (f g : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = 5 * x + 3) (h\u2081 : \u2200 x, g x = x ^ 2 - 2) :\n g (f (-1)) = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_326", "statement": "theorem mathd_numbertheory_326 (n : \u2115) (h\u2080 : (\u2191n - 1) * \u2191n * (\u2191n + 1) = (720 : \u2124)) : n + 1 = 10", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "induction_divisibility_3div2tooddnp1", "statement": "theorem induction_divisibility_3div2tooddnp1 (n : \u2115) : 3 \u2223 2 ^ (2 * n + 1) + 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_123", "statement": "theorem mathd_algebra_123 (a b : \u2115) (h\u2080 : 0 < a \u2227 0 < b) (h\u2081 : a + b = 20) (h\u2082 : a = 3 * b) :\n a - b = 10", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_2varlineareq_xpeeq7_2xpeeq3_eeq11_xeqn4", "statement": "theorem algebra_2varlineareq_xpeeq7_2xpeeq3_eeq11_xeqn4 (x e : \u2102) (h\u2080 : x + e = 7)\n (h\u2081 : 2 * x + e = 3) : e = 11 \u2227 x = -4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1993_p5", "statement": "theorem imo_1993_p5 : \u2203 f : \u2115 \u2192 \u2115, f 1 = 2 \u2227 \u2200 n, f (f n) = f n + n \u2227 \u2200 n, f n < f (n + 1)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "numbertheory_prmdvsneqnsqmodpeq0", "statement": "theorem numbertheory_prmdvsneqnsqmodpeq0 (n : \u2124) (p : \u2115) (h\u2080 : Nat.Prime p) :\n \u2191p \u2223 n \u2194 n ^ 2 % p = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1964_p1_1", "statement": "theorem imo_1964_p1_1 (n : \u2115) (h\u2080 : 7 \u2223 2 ^ n - 1) : 3 \u2223 n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1990_p3", "statement": "theorem imo_1990_p3 (n : \u2115) (h\u2080 : 2 \u2264 n) (h\u2081 : n ^ 2 \u2223 2 ^ n + 1) : n = 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "induction_ineq_nsqlefactn", "statement": "theorem induction_ineq_nsqlefactn (n : \u2115) (h\u2080 : 4 \u2264 n) : n ^ 2 \u2264 n !", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_30", "statement": "theorem mathd_numbertheory_30 :\n (33818 ^ 2 + 33819 ^ 2 + 33820 ^ 2 + 33821 ^ 2 + 33822 ^ 2) % 17 = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_267", "statement": "theorem mathd_algebra_267 (x : \u211d) (h\u2080 : x \u2260 1) (h\u2081 : x \u2260 -2)\n (h\u2082 : (x + 1) / (x - 1) = (x - 2) / (x + 2)) : x = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_961", "statement": "theorem mathd_numbertheory_961 : 2003 % 11 = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "induction_seq_mul2pnp1", "statement": "theorem induction_seq_mul2pnp1 (n : \u2115) (u : \u2115 \u2192 \u2115) (h\u2080 : u 0 = 0)\n (h\u2081 : \u2200 n, u (n + 1) = 2 * u n + (n + 1)) : u n = 2 ^ (n + 1) - (n + 2)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2002_p12", "statement": "theorem amc12a_2002_p12 (f : \u211d \u2192 \u211d) (k : \u211d) (a b : \u2115) (h\u2080 : \u2200 x, f x = x ^ 2 - 63 * x + k)\n (h\u2081 : f a = 0 \u2227 f b = 0) (h\u2082 : a \u2260 b) (h\u2083 : Nat.Prime a \u2227 Nat.Prime b) : k = 122", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_manipexpr_2erprsqpesqeqnrpnesq", "statement": "theorem algebra_manipexpr_2erprsqpesqeqnrpnesq (e r : \u2102) :\n 2 * (e * r) + (e ^ 2 + r ^ 2) = (-r + -e) ^ 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_119", "statement": "theorem mathd_algebra_119 (d e : \u211d) (h\u2080 : 2 * d = 17 * e - 8) (h\u2081 : 2 * e = d - 9) : e = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2020_p13", "statement": "theorem amc12a_2020_p13 (a b c : \u2115) (n : NNReal) (h\u2080 : n \u2260 1) (h\u2081 : 1 < a \u2227 1 < b \u2227 1 < c)\n (h\u2082 : (n * (n * n ^ (1 / c)) ^ (1 / b)) ^ (1 / a) = (n ^ 25) ^ (1 / 36)) : b = 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1977_p5", "statement": "theorem imo_1977_p5 (a b q r : \u2115) (h\u2080 : r < a + b) (h\u2081 : a ^ 2 + b ^ 2 = (a + b) * q + r)\n (h\u2082 : q ^ 2 + r = 1977) :\n abs ((a : \u2124) - 22) = 15 \u2227 abs ((b : \u2124) - 22) = 28 \u2228\n abs ((a : \u2124) - 22) = 28 \u2227 abs ((b : \u2124) - 22) = 15", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "numbertheory_2dvd4expn", "statement": "theorem numbertheory_2dvd4expn (n : \u2115) (h\u2080 : n \u2260 0) : 2 \u2223 4 ^ n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2010_p11", "statement": "theorem amc12a_2010_p11 (x b : \u211d) (h\u2080 : 0 < b) (h\u2081 : (7 : \u211d) ^ (x + 7) = 8 ^ x)\n (h\u2082 : x = Real.logb b (7 ^ 7)) : b = 8 / 7", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2003_p24", "statement": "theorem amc12a_2003_p24 :\n IsGreatest { y : \u211d | \u2203 a b : \u211d, 1 < b \u2227 b \u2264 a \u2227 y = Real.logb a (a / b) + Real.logb b (b / a) }\n 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2002_p1", "statement": "theorem amc12a_2002_p1 (f : \u2102 \u2192 \u2102) (h\u2080 : \u2200 x, f x = (2 * x + 3) * (x - 4) + (2 * x + 3) * (x - 6))\n (h\u2081 : Fintype (f \u207b\u00b9' {0})) : (\u2211 y in (f \u207b\u00b9' {0}).toFinset, y) = 7 / 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_206", "statement": "theorem mathd_algebra_206 (a b : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = x ^ 2 + a * x + b) (h\u2081 : 2 * a \u2260 b)\n (h\u2082 : f (2 * a) = 0) (h\u2083 : f b = 0) : a + b = -1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_92", "statement": "theorem mathd_numbertheory_92 (n : \u2115) (h\u2080 : 5 * n % 17 = 8) : n % 17 = 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_482", "statement": "theorem mathd_algebra_482 (m n : \u2115) (k : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : Nat.Prime m) (h\u2081 : Nat.Prime n)\n (h\u2082 : \u2200 x, f x = x ^ 2 - 12 * x + k) (h\u2083 : f m = 0) (h\u2084 : f n = 0) (h\u2085 : m \u2260 n) : k = 35", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12b_2002_p3", "statement": "theorem amc12b_2002_p3 (S : Finset \u2115)\n -- note: we use (n^2 + 2 - 3 * n) over (n^2 - 3 * n + 2) because nat subtraction truncates the latter at 1 and 2\n (h\u2080 : \u2200 n : \u2115, n \u2208 S \u2194 0 < n \u2227 Nat.Prime (n ^ 2 + 2 - 3 * n)) :\n S.card = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_668", "statement": "theorem mathd_numbertheory_668 (l r : ZMod 7) (h\u2080 : l = (2 + 3)\u207b\u00b9) (h\u2081 : r = 2\u207b\u00b9 + 3\u207b\u00b9) :\n l - r = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_251", "statement": "theorem mathd_algebra_251 (x : \u211d) (h\u2080 : x \u2260 0) (h\u2081 : 3 + 1 / x = 7 / x) : x = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_84", "statement": "theorem mathd_numbertheory_84 : Int.floor ((9 : \u211d) / 160 * 100) = 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_412", "statement": "theorem mathd_numbertheory_412 (x y : \u2115) (h\u2080 : x % 19 = 4) (h\u2081 : y % 19 = 7) :\n (x + 1) ^ 2 * (y + 5) ^ 3 % 19 = 13", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_181", "statement": "theorem mathd_algebra_181 (n : \u211d) (h\u2080 : n \u2260 3) (h\u2081 : (n + 5) / (n - 3) = 2) : n = 11", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2016_p3", "statement": "theorem amc12a_2016_p3 (f : \u211d \u2192 \u211d \u2192 \u211d)\n (h\u2080 : \u2200 x, \u2200 (y) (_ : y \u2260 0), f x y = x - y * Int.floor (x / y)) :\n f (3 / 8) (-(2 / 5)) = -(1 / 40)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_247", "statement": "theorem mathd_algebra_247 (t s : \u211d) (n : \u2124) (h\u2080 : t = 2 * s - s ^ 2) (h\u2081 : s = n ^ 2 - 2 ^ n + 1)\n (n) (_ : n = 3) : t = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_sqineq_2unitcircatblt1", "statement": "theorem algebra_sqineq_2unitcircatblt1 (a b : \u211d) (h\u2080 : a ^ 2 + b ^ 2 = 2) : a * b \u2264 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_629", "statement": "theorem mathd_numbertheory_629 : IsLeast { t : \u2115 | 0 < t \u2227 Nat.lcm 12 t ^ 3 = (12 * t) ^ 2 } 18", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "amc12a_2017_p2", "statement": "theorem amc12a_2017_p2 (x y : \u211d) (h\u2080 : x \u2260 0) (h\u2081 : y \u2260 0) (h\u2082 : x + y = 4 * (x * y)) :\n 1 / x + 1 / y = 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "algebra_amgm_sumasqdivbsqgeqsumbdiva", "statement": "theorem algebra_amgm_sumasqdivbsqgeqsumbdiva (a b c : \u211d) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c) :\n a ^ 2 / b ^ 2 + b ^ 2 / c ^ 2 + c ^ 2 / a ^ 2 \u2265 b / a + c / b + a / c", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_numbertheory_202", "statement": "theorem mathd_numbertheory_202 : (19 ^ 19 + 99 ^ 99) % 10 = 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "imo_1979_p1", "statement": "theorem imo_1979_p1 (p q : \u2115) (h\u2080 : 0 < q)\n (h\u2081 : (\u2211 k in Finset.Icc (1 : \u2115) 1319, (-1) ^ (k + 1) * ((1 : \u211d) / k)) = p / q) : 1979 \u2223 p", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_51", "statement": "theorem mathd_algebra_51 (a b : \u211d) (h\u2080 : 0 < a \u2227 0 < b) (h\u2081 : a + b = 35) (h\u2082 : a = 2 / 5 * b) :\n b - a = 15", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_10", "statement": "theorem mathd_algebra_10 : abs ((120 : \u211d) / 100 * 30 - 130 / 100 * 20) = 10", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Validation.lean", "split": "valid"} +{"full_name": "mathd_algebra_478", "statement": "theorem mathd_algebra_478 (b h v : \u211d) (h\u2080 : 0 < b \u2227 0 < h \u2227 0 < v) (h\u2081 : v = 1 / 3 * (b * h))\n (h\u2082 : b = 30) (h\u2083 : h = 13 / 2) : v = 65", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "numbertheory_4x3m7y3neq2003", "statement": "theorem numbertheory_4x3m7y3neq2003 (x y : \u2124) : 4 * x ^ 3 - 7 * y ^ 3 \u2260 2003", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1983_p1", "statement": "theorem aime_1983_p1 (x y z w : \u2115) (ht : 1 < x \u2227 1 < y \u2227 1 < z) (hw : 0 \u2264 w)\n (h0 : Real.log w / Real.log x = 24) (h1 : Real.log w / Real.log y = 40)\n (h2 : Real.log w / Real.log (x * y * z) = 12) : Real.log w / Real.log z = 60", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12_2001_p5", "statement": "theorem amc12_2001_p5 :\n Finset.prod (Finset.filter (fun x => \u00acEven x) (Finset.range 10000)) (id : \u2115 \u2192 \u2115) =\n 10000! / (2 ^ 5000 * 5000!)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_141", "statement": "theorem mathd_algebra_141 (a b : \u211d) (h\u2081 : a * b = 180) (h\u2082 : 2 * (a + b) = 54) :\n a ^ 2 + b ^ 2 = 369", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_3", "statement": "theorem mathd_numbertheory_3 : (\u2211 x in Finset.range 10, (x + 1) ^ 2) % 10 = 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1969_p2", "statement": "theorem imo_1969_p2 (m n : \u211d) (k : \u2115) (a : \u2115 \u2192 \u211d) (y : \u211d \u2192 \u211d) (h\u2080 : 0 < k)\n (h\u2081 : \u2200 x, y x = \u2211 i in Finset.range k, Real.cos (a i + x) / 2 ^ i) (h\u2082 : y m = 0)\n (h\u2083 : y n = 0) : \u2203 t : \u2124, m - n = t * \u03c0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_209", "statement": "theorem mathd_algebra_209 (\u03c3 : Equiv \u211d \u211d) (h\u2080 : \u03c3.2 2 = 10) (h\u2081 : \u03c3.2 10 = 1) (h\u2082 : \u03c3.2 1 = 2) :\n \u03c3.1 (\u03c3.1 10) = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_1124", "statement": "theorem mathd_numbertheory_1124 (n : \u2115) (h\u2080 : n \u2264 9) (h\u2081 : 18 \u2223 374 * 10 + n) : n = 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1983_p6", "statement": "theorem imo_1983_p6 (a b c : \u211d) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c) (h\u2081 : c < a + b) (h\u2082 : b < a + c)\n (h\u2083 : a < b + c) : 0 \u2264 a ^ 2 * b * (a - b) + b ^ 2 * c * (b - c) + c ^ 2 * a * (c - a)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_237", "statement": "theorem mathd_numbertheory_237 : (\u2211 k in Finset.range 101, k) % 6 = 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_33", "statement": "theorem mathd_algebra_33 (x y z : \u211d) (h\u2080 : x \u2260 0) (h\u2081 : 2 * x = 5 * y) (h\u2082 : 7 * y = 10 * z) :\n z / x = 7 / 25", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2021_p3", "statement": "theorem amc12b_2021_p3 (x : \u211d) (h\u2080 : 2 + 1 / (1 + 1 / (2 + 2 / (3 + x))) = 144 / 53) : x = 3 / 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_299", "statement": "theorem mathd_numbertheory_299 : 1 * 3 * 5 * 7 * 9 * 11 * 13 % 10 = 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2020_p2", "statement": "theorem amc12b_2020_p2 :\n (100 ^ 2 - 7 ^ 2 : \u211d) / (70 ^ 2 - 11 ^ 2) * ((70 - 11) * (70 + 11) / ((100 - 7) * (100 + 7))) =\n 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_sqineq_unitcircatbpabsamblt1", "statement": "theorem algebra_sqineq_unitcircatbpabsamblt1 (a b : \u211d) (h\u2080 : a ^ 2 + b ^ 2 = 1) :\n a * b + abs (a - b) \u2264 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1977_p6", "statement": "theorem imo_1977_p6 (f : \u2115 \u2192 \u2115) (h\u2080 : \u2200 n, 0 < f n) (h\u2081 : \u2200 n, 0 < n \u2192 f (f n) < f (n + 1)) :\n \u2200 n, 0 < n \u2192 f n = n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_419", "statement": "theorem mathd_algebra_419 (a b : \u211d) (h\u2080 : a = -1) (h\u2081 : b = 5) : -a - b ^ 2 + 3 * (a * b) = -39", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2020_p10", "statement": "theorem amc12a_2020_p10 (n : \u2115) (h\u2080 : 0 < n)\n (h\u2081 : Real.logb 2 (Real.logb 16 n) = Real.logb 4 (Real.logb 4 n)) :\n (Nat.digits 10 n).sum = 13", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1960_p2", "statement": "theorem imo_1960_p2 (x : \u211d) (h\u2080 : 0 \u2264 1 + 2 * x) (h\u2081 : (1 - Real.sqrt (1 + 2 * x)) ^ 2 \u2260 0)\n (h\u2082 : 4 * x ^ 2 / (1 - Real.sqrt (1 + 2 * x)) ^ 2 < 2 * x + 9) : -(1 / 2) \u2264 x \u2227 x < 45 / 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_427", "statement": "theorem mathd_numbertheory_427 (a : \u2115) (h\u2080 : a = \u2211 k in Nat.divisors 500, k) :\n (\u2211 k in Finset.filter (fun x => Nat.Prime x) (Nat.divisors a), k) = 25", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "numbertheory_x5neqy2p4", "statement": "theorem numbertheory_x5neqy2p4 (x y : \u2124) : x ^ 5 \u2260 y ^ 2 + 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imosl_2007_algebra_p6", "statement": "theorem imosl_2007_algebra_p6 (a : \u2115 \u2192 NNReal) (h\u2080 : (\u2211 x in Finset.range 100, a (x + 1) ^ 2) = 1) :\n (\u2211 x in Finset.range 99, a (x + 1) ^ 2 * a (x + 2)) + a 100 ^ 2 * a 1 < 12 / 25", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_398", "statement": "theorem mathd_algebra_398 (a b c : \u211d) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c) (h\u2081 : 9 * b = 20 * c)\n (h\u2082 : 7 * a = 4 * b) : 63 * a = 80 * c", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1963_p5", "statement": "theorem imo_1963_p5 : Real.cos (\u03c0 / 7) - Real.cos (2 * \u03c0 / 7) + Real.cos (3 * \u03c0 / 7) = 1 / 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_430", "statement": "theorem mathd_numbertheory_430 (a b c : \u2115) (h\u2080 : 1 \u2264 a \u2227 a \u2264 9) (h\u2081 : 1 \u2264 b \u2227 b \u2264 9)\n (h\u2082 : 1 \u2264 c \u2227 c \u2264 9) (h\u2083 : a \u2260 b) (h\u2084 : a \u2260 c) (h\u2085 : b \u2260 c) (h\u2086 : a + b = c)\n (h\u2087 : 10 * a + a - b = 2 * c) (h\u2088 : c * b = 10 * a + a + a) : a + b + c = 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_459", "statement": "theorem mathd_algebra_459 (a b c d : \u211a) (h\u2080 : 3 * a = b + c + d) (h\u2081 : 4 * b = a + c + d)\n (h\u2082 : 2 * c = a + b + d) (h\u2083 : 8 * a + 10 * b + 6 * c = 24) : \u2191d.den + d.num = 28", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "induction_12dvd4expnp1p20", "statement": "theorem induction_12dvd4expnp1p20 (n : \u2115) : 12 \u2223 4 ^ (n + 1) + 20", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_320", "statement": "theorem mathd_algebra_320 (x : \u211d) (a b c : \u2115) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c \u2227 0 \u2264 x)\n (h\u2081 : 2 * x ^ 2 = 4 * x + 9) (h\u2082 : x = (a + Real.sqrt b) / c) (h\u2083 : c = 2) : a + b + c = 26", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_137", "statement": "theorem mathd_algebra_137 (x : \u2115) (h\u2080 : \u2191x + (4 : \u211d) / (100 : \u211d) * \u2191x = 598) : x = 575", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1997_p5", "statement": "theorem imo_1997_p5 (x y : \u2115) (h\u2080 : 0 < x \u2227 0 < y) (h\u2081 : x ^ y ^ 2 = y ^ x) :\n (x, y) = (1, 1) \u2228 (x, y) = (16, 2) \u2228 (x, y) = (27, 3)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_277", "statement": "theorem mathd_numbertheory_277 (m n : \u2115) (h\u2080 : Nat.gcd m n = 6) (h\u2081 : Nat.lcm m n = 126) :\n 60 \u2264 m + n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_559", "statement": "theorem mathd_numbertheory_559 (x y : \u2115) (h\u2080 : x % 3 = 2) (h\u2081 : y % 5 = 4) (h\u2082 : x % 10 = y % 10) :\n 14 \u2264 x", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_160", "statement": "theorem mathd_algebra_160 (n x : \u211d) (h\u2080 : n + x = 97) (h\u2081 : n + 5 * x = 265) : n + 2 * x = 139", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_24", "statement": "theorem mathd_algebra_24 (x : \u211d) (h\u2080 : x / 50 = 40) : x = 2000", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_176", "statement": "theorem mathd_algebra_176 (x : \u211d) : (x + 1) ^ 2 * x = x ^ 3 + 2 * x ^ 2 + x", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "induction_nfactltnexpnm1ngt3", "statement": "theorem induction_nfactltnexpnm1ngt3 (n : \u2115) (h\u2080 : 3 \u2264 n) : n ! < n ^ (n - 1)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_208", "statement": "theorem mathd_algebra_208 : Real.sqrt 1000000 - 1000000 ^ ((1 : \u211d) / 3) = 900", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_353", "statement": "theorem mathd_numbertheory_353 (s : \u2115) (h\u2080 : s = \u2211 k in Finset.Icc 2010 4018, k) : s % 2009 = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "numbertheory_notequiv2i2jasqbsqdiv8", "statement": "theorem numbertheory_notequiv2i2jasqbsqdiv8 :\n \u00ac\u2200 a b : \u2124, (\u2203 i j, a = 2 * i \u2227 b = 2 * j) \u2194 \u2203 k, a ^ 2 + b ^ 2 = 8 * k", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_156", "statement": "theorem mathd_algebra_156 (x y : \u211d) (f g : \u211d \u2192 \u211d) (h\u2080 : \u2200 t, f t = t ^ 4)\n (h\u2081 : \u2200 t, g t = 5 * t ^ 2 - 6) (h\u2082 : f x = g x) (h\u2083 : f y = g y) (h\u2084 : x ^ 2 < y ^ 2) :\n y ^ 2 - x ^ 2 = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_12", "statement": "theorem mathd_numbertheory_12 :\n Finset.card (Finset.filter (fun x => 20 \u2223 x) (Finset.Icc 15 85)) = 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_345", "statement": "theorem mathd_numbertheory_345 : (2000 + 2001 + 2002 + 2003 + 2004 + 2005 + 2006) % 7 = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_447", "statement": "theorem mathd_numbertheory_447 :\n (\u2211 k in Finset.filter (fun x => 3 \u2223 x) (Finset.Icc 1 49), k % 10) = 78", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_328", "statement": "theorem mathd_numbertheory_328 : 5 ^ 999999 % 7 = 6", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_451", "statement": "theorem mathd_numbertheory_451 (S : Finset \u2115)\n (h\u2080 :\n \u2200 n : \u2115,\n n \u2208 S \u2194\n 2010 \u2264 n \u2227 n \u2264 2019 \u2227 \u2203 m, (Nat.divisors m).card = 4 \u2227 (\u2211 p in Nat.divisors m, p) = n) :\n (\u2211 k in S, k) = 2016", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1997_p9", "statement": "theorem aime_1997_p9 (a : \u211d) (h\u2080 : 0 < a)\n (h\u2081 : 1 / a - Int.floor (1 / a) = a ^ 2 - Int.floor (a ^ 2)) (h\u2082 : 2 < a ^ 2) (h\u2083 : a ^ 2 < 3) :\n a ^ 12 - 144 * (1 / a) = 233", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_sqineq_at2malt1", "statement": "theorem algebra_sqineq_at2malt1 (a : \u211d) : a * (2 - a) \u2264 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_apbmpcneq0_aeq0anbeq0anceq0", "statement": "theorem algebra_apbmpcneq0_aeq0anbeq0anceq0 (a b c : \u211a) (m n : \u211d) (h\u2080 : 0 < m \u2227 0 < n)\n (h\u2081 : m ^ 3 = 2) (h\u2082 : n ^ 3 = 4) (h\u2083 : (a : \u211d) + b * m + c * n = 0) : a = 0 \u2227 b = 0 \u2227 c = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_171", "statement": "theorem mathd_algebra_171 (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = 5 * x + 4) : f 1 = 9", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_227", "statement": "theorem mathd_numbertheory_227 (x y n : \u2115+) (h\u2080 : \u2191x / (4 : \u211d) + y / 6 = (x + y) / n) : n = 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_188", "statement": "theorem mathd_algebra_188 (\u03c3 : Equiv \u211d \u211d) (h : \u03c3.1 2 = \u03c3.2 2) : \u03c3.1 (\u03c3.1 2) = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_765", "statement": "theorem mathd_numbertheory_765 (x : \u2124) (h\u2080 : x < 0) (h\u2081 : 24 * x % 1199 = 15) : x \u2264 -449", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1959_p1", "statement": "theorem imo_1959_p1 (n : \u2115) (h\u2080 : 0 < n) : Nat.gcd (21 * n + 4) (14 * n + 3) = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_175", "statement": "theorem mathd_numbertheory_175 : 2 ^ 2010 % 10 = 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "induction_sumkexp3eqsumksq", "statement": "theorem induction_sumkexp3eqsumksq (n : \u2115) :\n (\u2211 k in Finset.range n, k ^ 3) = (\u2211 k in Finset.range n, k) ^ 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown", "statement": "theorem numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown (m n : \u2115) (f : \u2115 \u2192 \u2115)\n (h\u2080 : \u2200 x, f x = 4 ^ x + 6 ^ x + 9 ^ x) (h\u2081 : 0 < m \u2227 0 < n) (h\u2082 : m \u2264 n) :\n f (2 ^ m) \u2223 f (2 ^ n)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1992_p1", "statement": "theorem imo_1992_p1 (p q r : \u2124) (h\u2080 : 1 < p \u2227 p < q \u2227 q < r)\n (h\u2081 : (p - 1) * (q - 1) * (r - 1) \u2223 p * q * r - 1) :\n (p, q, r) = (2, 4, 8) \u2228 (p, q, r) = (3, 5, 15)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1982_p1", "statement": "theorem imo_1982_p1 (f : \u2115 \u2192 \u2115)\n (h\u2080 : \u2200 m n, 0 < m \u2227 0 < n \u2192 f (m + n) - f m - f n = 0 \u2228 f (m + n) - f m - f n = 1)\n (h\u2081 : f 2 = 0) (h\u2082 : 0 < f 3) (h\u2083 : f 9999 = 3333) : f 1982 = 660", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1987_p5", "statement": "theorem aime_1987_p5 (x y : \u2124) (h\u2080 : y ^ 2 + 3 * (x ^ 2 * y ^ 2) = 30 * x ^ 2 + 517) :\n 3 * (x ^ 2 * y ^ 2) = 588", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_346", "statement": "theorem mathd_algebra_346 (f g : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = 2 * x - 3) (h\u2081 : \u2200 x, g x = x + 1) :\n g (f 5 - 1) = 7", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_487", "statement": "theorem mathd_algebra_487 (a b c d : \u211d) (h\u2080 : b = a ^ 2) (h\u2081 : a + b = 1) (h\u2082 : d = c ^ 2)\n (h\u2083 : c + d = 1) (h\u2084 : a \u2260 c) : Real.sqrt ((a - c) ^ 2 + (b - d) ^ 2) = Real.sqrt 10", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_728", "statement": "theorem mathd_numbertheory_728 : (29 ^ 13 - 5 ^ 13) % 7 = 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_184", "statement": "theorem mathd_algebra_184 (a b : NNReal) (h\u2080 : 0 < a \u2227 0 < b) (h\u2081 : a ^ 2 = 6 * b)\n (h\u2082 : a ^ 2 = 54 / b) : a = 3 * NNReal.sqrt 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_552", "statement": "theorem mathd_numbertheory_552 (f g h : \u2115+ \u2192 \u2115) (h\u2080 : \u2200 x, f x = 12 * x + 7)\n (h\u2081 : \u2200 x, g x = 5 * x + 2) (h\u2082 : \u2200 x, h x = Nat.gcd (f x) (g x)) (h\u2083 : Fintype (Set.range h)) :\n (\u2211 k in (Set.range h).toFinset, k) = 12", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2021_p9", "statement": "theorem amc12b_2021_p9 :\n Real.log 80 / Real.log 2 / (Real.log 2 / Real.log 40) -\n Real.log 160 / Real.log 2 / (Real.log 2 / Real.log 20) =\n 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1994_p3", "statement": "theorem aime_1994_p3 (x : \u2124) (f : \u2124 \u2192 \u2124) (h0 : f x + f (x - 1) = x ^ 2) (h1 : f 19 = 94) :\n f 94 % 1000 = 561", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_44", "statement": "theorem mathd_algebra_44 (s t : \u211d) (h\u2080 : s = 9 - 2 * t) (h\u2081 : t = 3 * s + 1) : s = 1 \u2227 t = 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_215", "statement": "theorem mathd_algebra_215 (S : Finset \u211d) (h\u2080 : \u2200 x : \u211d, x \u2208 S \u2194 (x + 3) ^ 2 = 121) :\n (\u2211 k in S, k) = -6", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_293", "statement": "theorem mathd_numbertheory_293 (n : \u2115) (h\u2080 : n \u2264 9) (h\u2081 : 11 \u2223 20 * 100 + 10 * n + 7) : n = 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_769", "statement": "theorem mathd_numbertheory_769 : (129 ^ 34 + 96 ^ 38) % 11 = 9", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_452", "statement": "theorem mathd_algebra_452 (a : \u2115 \u2192 \u211d) (h\u2080 : \u2200 n, a (n + 2) - a (n + 1) = a (n + 1) - a n)\n (h\u2081 : a 1 = 2 / 3) (h\u2082 : a 9 = 4 / 5) : a 5 = 11 / 15", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_5", "statement": "theorem mathd_numbertheory_5 (n : \u2115) (h\u2080 : 10 \u2264 n) (h\u2081 : \u2203 x, x ^ 2 = n) (h\u2082 : \u2203 t, t ^ 3 = n) :\n 64 \u2264 n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_207", "statement": "theorem mathd_numbertheory_207 : 8 * 9 ^ 2 + 5 * 9 + 2 = 695", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_342", "statement": "theorem mathd_numbertheory_342 : 54 % 6 = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_483", "statement": "theorem mathd_numbertheory_483 (a : \u2115 \u2192 \u2115) (h\u2080 : a 1 = 1) (h\u2081 : a 2 = 1)\n (h\u2082 : \u2200 n, a (n + 2) = a (n + 1) + a n) : a 100 % 4 = 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2020_p21", "statement": "theorem amc12b_2020_p21 (S : Finset \u2115)\n (h\u2080 : \u2200 n : \u2115, n \u2208 S \u2194 0 < n \u2227 (\u2191n + (1000 : \u211d)) / 70 = Int.floor (Real.sqrt n)) : S.card = 6", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2003_p5", "statement": "theorem amc12a_2003_p5 (A M C : \u2115) (h\u2080 : A \u2264 9 \u2227 M \u2264 9 \u2227 C \u2264 9)\n (h\u2081 : Nat.ofDigits 10 [0, 1, C, M, A] + Nat.ofDigits 10 [2, 1, C, M, A] = 123422) :\n A + M + C = 14", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_495", "statement": "theorem mathd_numbertheory_495 (a b : \u2115) (h\u2080 : 0 < a \u2227 0 < b) (h\u2081 : a % 10 = 2) (h\u2082 : b % 10 = 4)\n (h\u2083 : Nat.gcd a b = 6) : 108 \u2264 Nat.lcm a b", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_296", "statement": "theorem mathd_algebra_296 : abs ((3491 - 60) * (3491 + 60) - 3491 ^ 2 : \u2124) = 3600", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2", "statement": "theorem algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2 (a b c : \u211d) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c)\n (h\u2081 : 3 \u2264 a * b + b * c + c * a) :\n 3 / Real.sqrt 2 \u2264 a / Real.sqrt (a + b) + b / Real.sqrt (b + c) + c / Real.sqrt (c + a)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_2varlineareq_fp3zeq11_3tfm1m5zeqn68_feqn10_zeq7", "statement": "theorem algebra_2varlineareq_fp3zeq11_3tfm1m5zeqn68_feqn10_zeq7 (f z : \u2102) (h\u2080 : f + 3 * z = 11)\n (h\u2081 : 3 * (f - 1) - 5 * z = -68) : f = -10 \u2227 z = 7", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_247", "statement": "theorem mathd_numbertheory_247 (n : \u2115) (h\u2080 : 3 * n % 2 = 11) : n % 11 = 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "induction_pord1p1on2powklt5on2", "statement": "theorem induction_pord1p1on2powklt5on2 (n : \u2115) (h\u2080 : 0 < n) :\n (\u220f k in Finset.Icc 1 n, 1 + (1 : \u211d) / 2 ^ k) < 5 / 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_107", "statement": "theorem mathd_algebra_107 (x y : \u211d) (h\u2080 : x ^ 2 + 8 * x + y ^ 2 - 6 * y = 0) :\n (x + 4) ^ 2 + (y - 3) ^ 2 = 5 ^ 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "numbertheory_2pownm1prime_nprime", "statement": "theorem numbertheory_2pownm1prime_nprime (n : \u2115) (h\u2080 : 0 < n) (h\u2081 : Nat.Prime (2 ^ n - 1)) :\n Nat.Prime n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_412", "statement": "theorem mathd_algebra_412 (x y : \u211d) (h\u2080 : x + y = 25) (h\u2081 : x - y = 11) : x = 18", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2013_p4", "statement": "theorem amc12a_2013_p4 : (2 ^ 2014 + 2 ^ 2012) / (2 ^ 2014 - 2 ^ 2012) = (5 : \u211d) / 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_392", "statement": "theorem mathd_algebra_392 (n : \u2115) (h\u2080 : Even n)\n (h\u2081 : (\u2191n - 2) ^ 2 + \u2191n ^ 2 + (\u2191n + 2) ^ 2 = (12296 : \u2115)) :\n (\u2191n - 2) * \u2191n * (\u2191n + 2) / 8 = (32736 : \u2115)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_314", "statement": "theorem mathd_numbertheory_314 (r n : \u2115) (h\u2080 : r = 1342 % 13) (h\u2081 : 0 < n) (h\u2082 : 1342 \u2223 n)\n (h\u2083 : n % 13 < r) : 6710 \u2264 n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "induction_prod1p1onk3le3m1onn", "statement": "theorem induction_prod1p1onk3le3m1onn (n : \u2115) (h\u2080 : 0 < n) :\n (\u220f k in Finset.Icc 1 n, 1 + (1 : \u211d) / k ^ 3) \u2264 (3 : \u211d) - 1 / \u2191n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_343", "statement": "theorem mathd_numbertheory_343 : (\u220f k in Finset.range 6, 2 * k + 1) % 10 = 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_756", "statement": "theorem mathd_algebra_756 (a b : \u211d) (h\u2080 : (2 : \u211d) ^ a = 32) (h\u2081 : a ^ b = 125) : b ^ a = 243", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2002_p7", "statement": "theorem amc12b_2002_p7 (a b c : \u2115) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c) (h\u2081 : b = a + 1) (h\u2082 : c = b + 1)\n (h\u2083 : a * b * c = 8 * (a + b + c)) : a ^ 2 + (b ^ 2 + c ^ 2) = 77", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_80", "statement": "theorem mathd_algebra_80 (x : \u211d) (h\u2080 : x \u2260 -1) (h\u2081 : (x - 9) / (x + 1) = 2) : x = -11", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_457", "statement": "theorem mathd_numbertheory_457 (n : \u2115) (h\u2080 : 0 < n) (h\u2081 : 80325 \u2223 n !) : 17 \u2264 n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12_2000_p12", "statement": "theorem amc12_2000_p12 (a m c : \u2115) (h\u2080 : a + m + c = 12) :\n a * m * c + a * m + m * c + a * c \u2264 112", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_135", "statement": "theorem mathd_numbertheory_135 (n A B C : \u2115) (h\u2080 : n = 3 ^ 17 + 3 ^ 10) (h\u2081 : 11 \u2223 n + 1)\n (h\u2082 : [A, B, C].Pairwise (\u00b7 \u2260 \u00b7)) (h\u2083 : {A, B, C} \u2282 Finset.Icc 0 9) (h\u2084 : Odd A \u2227 Odd C)\n (h\u2085 : \u00ac3 \u2223 B) (h\u2086 : Nat.digits 10 n = [B, A, B, C, C, A, C, B, A]) :\n 100 * A + 10 * B + C = 129", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_275", "statement": "theorem mathd_algebra_275 (x : \u211d) (h : ((11 : \u211d) ^ (1 / 4)) ^ (3 * x - 3) = 1 / 5) :\n ((11 : \u211d) ^ (1 / 4)) ^ (6 * x + 2) = 121 / 25", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_388", "statement": "theorem mathd_algebra_388 (x y z : \u211d) (h\u2080 : 3 * x + 4 * y - 12 * z = 10)\n (h\u2081 : -2 * x - 3 * y + 9 * z = -4) : x = 14", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2020_p7", "statement": "theorem amc12a_2020_p7 (a : \u2115 \u2192 \u2115) (h\u2080 : a 0 ^ 3 = 1) (h\u2081 : a 1 ^ 3 = 8) (h\u2082 : a 2 ^ 3 = 27)\n (h\u2083 : a 3 ^ 3 = 64) (h\u2084 : a 4 ^ 3 = 125) (h\u2085 : a 5 ^ 3 = 216) (h\u2086 : a 6 ^ 3 = 343) :\n \u2191(\u2211 k in Finset.range 7, 6 * a k ^ 2) - \u2191(2 * \u2211 k in Finset.range 6, a k ^ 2) = (658 : \u2124)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1981_p6", "statement": "theorem imo_1981_p6 (f : \u2115 \u2192 \u2115 \u2192 \u2115) (h\u2080 : \u2200 y, f 0 y = y + 1) (h\u2081 : \u2200 x, f (x + 1) 0 = f x 1)\n (h\u2082 : \u2200 x y, f (x + 1) (y + 1) = f x (f (x + 1) y)) : \u2200 y, f 4 (y + 1) = 2 ^ (f 4 y + 3) - 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_263", "statement": "theorem mathd_algebra_263 (y : \u211d) (h\u2080 : 0 \u2264 19 + 3 * y) (h\u2081 : Real.sqrt (19 + 3 * y) = 7) :\n y = 10", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_34", "statement": "theorem mathd_numbertheory_34 (x : \u2115) (h\u2080 : x < 100) (h\u2081 : x * 9 % 100 = 1) : x = 89", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_764", "statement": "theorem mathd_numbertheory_764 (p : \u2115) (h\u2080 : Nat.Prime p) (h\u2081 : 7 \u2264 p) :\n (\u2211 k in Finset.Icc 1 (p - 2), (k : ZMod p)\u207b\u00b9 * ((k : ZMod p) + 1)\u207b\u00b9) = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2021_p4", "statement": "theorem amc12b_2021_p4 (m a : \u2115) (h\u2080 : 0 < m \u2227 0 < a) (h\u2081 : \u2191m / \u2191a = (3 : \u211d) / 4) :\n (84 * \u2191m + 70 * \u2191a) / (\u2191m + \u2191a) = (76 : \u211d)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1962_p2", "statement": "theorem imo_1962_p2 (x : \u211d) (h\u2080 : 0 \u2264 3 - x) (h\u2081 : 0 \u2264 x + 1)\n (h\u2082 : 1 / 2 < Real.sqrt (3 - x) - Real.sqrt (x + 1)) : -1 \u2264 x \u2227 x < 1 - Real.sqrt 31 / 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_170", "statement": "theorem mathd_algebra_170 (S : Finset \u2124) (h\u2080 : \u2200 n : \u2124, n \u2208 S \u2194 abs (n - 2) \u2264 5 + 6 / 10) :\n S.card = 11", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_432", "statement": "theorem mathd_algebra_432 (x : \u211d) : (x + 3) * (2 * x - 6) = 2 * x ^ 2 - 18", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_598", "statement": "theorem mathd_algebra_598 (a b c d : \u211d) (h\u2081 : (4 : \u211d) ^ a = 5) (h\u2082 : (5 : \u211d) ^ b = 6)\n (h\u2083 : (6 : \u211d) ^ c = 7) (h\u2084 : (7 : \u211d) ^ d = 8) : a * b * c * d = 3 / 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_bleqa_apbon2msqrtableqambsqon8b", "statement": "theorem algebra_bleqa_apbon2msqrtableqambsqon8b (a b : \u211d) (h\u2080 : 0 < a \u2227 0 < b) (h\u2081 : b \u2264 a) :\n (a + b) / 2 - Real.sqrt (a * b) \u2264 (a - b) ^ 2 / (8 * b)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_276", "statement": "theorem mathd_algebra_276 (a b : \u2124)\n (h\u2080 : \u2200 x : \u211d, 10 * x ^ 2 - x - 24 = (a * x - 8) * (b * x + 3)) : a * b + b = 12", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2021_p14", "statement": "theorem amc12a_2021_p14 :\n ((\u2211 k:\u2124 in Finset.Icc 1 20, Real.logb (5 ^ k) (3 ^ k ^ 2)) *\n \u2211 k:\u2124 in Finset.Icc 1 100, Real.logb (9 ^ k) (25 ^ k)) =\n 21000", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_sum1onsqrt2to1onsqrt10000lt198", "statement": "theorem algebra_sum1onsqrt2to1onsqrt10000lt198 :\n (\u2211 k in Finset.Icc (2 : \u2115) 10000, 1 / Real.sqrt k) < 198", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_618", "statement": "theorem mathd_numbertheory_618 (n : \u2115) (p : \u2115 \u2192 \u2115) (h\u2080 : \u2200 x, p x = x ^ 2 - x + 41)\n (h\u2081 : 1 < Nat.gcd (p n) (p (n + 1))) : 41 \u2264 n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2020_p4", "statement": "theorem amc12a_2020_p4 (S : Finset \u2115)\n (h\u2080 : \u2200 n : \u2115, n \u2208 S \u2194 1000 \u2264 n \u2227 n \u2264 9999 \u2227 (\u2200 d : \u2115, d \u2208 Nat.digits 10 n \u2192 Even d) \u2227 5 \u2223 n) :\n S.card = 100", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2020_p6", "statement": "theorem amc12b_2020_p6 (n : \u2115) (h\u2080 : 9 \u2264 n) : \u2203 x : \u2115, (x : \u211d) ^ 2 = ((n + 2)! - (n + 1)!) / n !", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_435", "statement": "theorem mathd_numbertheory_435 (k : \u2115) (h\u2080 : 0 < k) (h\u2081 : \u2200 n, Nat.gcd (6 * n + k) (6 * n + 3) = 1)\n (h\u2082 : \u2200 n, Nat.gcd (6 * n + k) (6 * n + 2) = 1) (h\u2083 : \u2200 n, Nat.gcd (6 * n + k) (6 * n + 1) = 1) :\n 5 \u2264 k", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_others_exirrpowirrrat", "statement": "theorem algebra_others_exirrpowirrrat : \u2203 a b : \u211d, (Irrational a) \u2227 (Irrational b) \u2227 \u00ac(Irrational (a ^ b))", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_427", "statement": "theorem mathd_algebra_427 (x y z : \u211d) (h\u2080 : 3 * x + y = 17) (h\u2081 : 5 * y + z = 14)\n (h\u2082 : 3 * x + 5 * z = 41) : x + y + z = 12", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_76", "statement": "theorem mathd_algebra_76 (f : \u2124 \u2192 \u2124) (h\u2080 : \u2200 n, Odd n \u2192 f n = n ^ 2)\n (h\u2081 : \u2200 n, Even n \u2192 f n = n ^ 2 - 4 * n - 1) : f 4 = -1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_99", "statement": "theorem mathd_numbertheory_99 (n : \u2115) (h\u2080 : 2 * n % 47 = 15) : n % 47 = 31", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_9onxpypzleqsum2onxpy", "statement": "theorem algebra_9onxpypzleqsum2onxpy (x y z : \u211d) (h\u2080 : 0 < x \u2227 0 < y \u2227 0 < z) :\n 9 / (x + y + z) \u2264 2 / (x + y) + 2 / (y + z) + 2 / (z + x)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_233", "statement": "theorem mathd_numbertheory_233 (b : ZMod (11 ^ 2)) (h\u2080 : b = 24\u207b\u00b9) : b = 116", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_absapbon1pabsapbleqsumabsaon1pabsa", "statement": "theorem algebra_absapbon1pabsapbleqsumabsaon1pabsa (a b : \u211d) :\n abs (a + b) / (1 + abs (a + b)) \u2264 abs a / (1 + abs a) + abs b / (1 + abs b)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1984_p6", "statement": "theorem imo_1984_p6 (a b c d k m : \u2115) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c \u2227 0 < d)\n (h\u2081 : Odd a \u2227 Odd b \u2227 Odd c \u2227 Odd d) (h\u2082 : a < b \u2227 b < c \u2227 c < d) (h\u2083 : a * d = b * c)\n (h\u2084 : a + d = 2 ^ k) (h\u2085 : b + c = 2 ^ m) : a = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_2001_p6", "statement": "theorem imo_2001_p6 (a b c d : \u2115) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c \u2227 0 < d) (h\u2081 : d < c) (h\u2082 : c < b)\n (h\u2083 : b < a) (h\u2084 : a * c + b * d = (b + d + a - c) * (b + d + c - a)) :\n \u00acNat.Prime (a * b + c * d)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_321", "statement": "theorem mathd_numbertheory_321 (n : ZMod 1399) (h\u2081 : n = 160\u207b\u00b9) : n = 1058", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_17", "statement": "theorem mathd_algebra_17 (a : \u211d)\n (h\u2080 : Real.sqrt (4 + Real.sqrt (16 + 16 * a)) + Real.sqrt (1 + Real.sqrt (1 + a)) = 6) :\n a = 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_153", "statement": "theorem mathd_algebra_153 (n : \u211d) (h\u2080 : n = 1 / 3) :\n Int.floor (10 * n) + Int.floor (100 * n) + Int.floor (1000 * n) + Int.floor (10000 * n) =\n 3702", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_sqineq_unitcircatbpamblt1", "statement": "theorem algebra_sqineq_unitcircatbpamblt1 (a b : \u211d) (h\u2080 : a ^ 2 + b ^ 2 = 1) :\n a * b + (a - b) \u2264 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2021_p18", "statement": "theorem amc12a_2021_p18 (f : \u211a \u2192 \u211d) (h\u2080 : \u2200 x > 0, \u2200 y > 0, f (x * y) = f x + f y)\n (h\u2081 : \u2200 p, Nat.Prime p \u2192 f p = p) : f (25 /. 11) < 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_329", "statement": "theorem mathd_algebra_329 (x y : \u211d) (h\u2080 : 3 * y = x) (h\u2081 : 2 * x + 5 * y = 11) : x + y = 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "induction_pprime_pdvdapowpma", "statement": "theorem induction_pprime_pdvdapowpma (p a : \u2115) (h\u2080 : 0 < a) (h\u2081 : Nat.Prime p) : p \u2223 a ^ p - a", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2021_p9", "statement": "theorem amc12a_2021_p9 : (\u220f k in Finset.range 7, 2 ^ 2 ^ k + 3 ^ 2 ^ k) = 3 ^ 128 - 2 ^ 128", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1984_p1", "statement": "theorem aime_1984_p1 (u : \u2115 \u2192 \u211a) (h\u2080 : \u2200 n, u (n + 1) = u n + 1)\n (h\u2081 : (\u2211 k in Finset.range 98, u k.succ) = 137) :\n (\u2211 k in Finset.range 49, u (2 * k.succ)) = 93", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2021_p22", "statement": "theorem amc12a_2021_p22 (a b c : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = x ^ 3 + a * x ^ 2 + b * x + c)\n (h\u2081 :\n f \u207b\u00b9' {0} =\n {Real.cos (2 * Real.pi / 7), Real.cos (4 * Real.pi / 7), Real.cos (6 * Real.pi / 7)}) :\n a * b * c = 1 / 32", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_229", "statement": "theorem mathd_numbertheory_229 : 5 ^ 30 % 7 = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_100", "statement": "theorem mathd_numbertheory_100 (n : \u2115) (h\u2080 : 0 < n) (h\u2081 : Nat.gcd n 40 = 10)\n (h\u2082 : Nat.lcm n 40 = 280) : n = 70", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_313", "statement": "theorem mathd_algebra_313 (v i z : \u2102) (h\u2080 : v = i * z) (h\u2081 : v = 1 + Complex.I)\n (h\u2082 : z = 2 - Complex.I) : i = 1 / 5 + 3 / 5 * Complex.I", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2002_p4", "statement": "theorem amc12b_2002_p4 (n : \u2115) (h\u2080 : 0 < n) (h\u2081 : (1 /. 2 + 1 /. 3 + 1 /. 7 + 1 /. \u2191n).den = 1) :\n n = 42", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2002_p6", "statement": "theorem amc12a_2002_p6 (n : \u2115) (h\u2080 : 0 < n) : \u2203 m, m > n \u2227 \u2203 p, m * p \u2264 m + p", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2003_p23", "statement": "theorem amc12a_2003_p23 (S : Finset \u2115)\n (h\u2080 : \u2200 k : \u2115, k \u2208 S \u2194 0 < k \u2227 (k * k : \u2115) \u2223 \u220f i in Finset.Icc 1 9, i !) : S.card = 672", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_129", "statement": "theorem mathd_algebra_129 (a : \u211d) (h\u2080 : a \u2260 0) (h\u2081 : 8\u207b\u00b9 / 4\u207b\u00b9 - a\u207b\u00b9 = 1) : a = -2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2021_p18", "statement": "theorem amc12b_2021_p18 (z : \u2102)\n (h\u2080 : 12 * Complex.normSq z = 2 * Complex.normSq (z + 2) + Complex.normSq (z ^ 2 + 1) + 31) :\n z + 6 / z = -2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_484", "statement": "theorem mathd_algebra_484 : Real.log 27 / Real.log 3 = 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_551", "statement": "theorem mathd_numbertheory_551 : 1529 % 6 = 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_304", "statement": "theorem mathd_algebra_304 : 91 ^ 2 = 8281", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2021_p8", "statement": "theorem amc12a_2021_p8 (d : \u2115 \u2192 \u2115) (h\u2080 : d 0 = 0) (h\u2081 : d 1 = 0) (h\u2082 : d 2 = 1)\n (h\u2083 : \u2200 n \u2265 3, d n = d (n - 1) + d (n - 3)) : Even (d 2021) \u2227 Odd (d 2022) \u2227 Even (d 2023)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_ineq_nto1onlt2m1on", "statement": "theorem algebra_ineq_nto1onlt2m1on (n : \u2115) : (n : \u211d) ^ ((1 : \u211d) / n) < 2 - 1 / n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2002_p19", "statement": "theorem amc12b_2002_p19 (a b c : \u211d) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c) (h\u2081 : a * (b + c) = 152)\n (h\u2082 : b * (c + a) = 162) (h\u2083 : c * (a + b) = 170) : a * b * c = 720", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_341", "statement": "theorem mathd_numbertheory_341 (a b c : \u2115) (h\u2080 : a \u2264 9 \u2227 b \u2264 9 \u2227 c \u2264 9)\n (h\u2081 : Nat.digits 10 (5 ^ 100 % 1000) = [c, b, a]) : a + b + c = 13", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_711", "statement": "theorem mathd_numbertheory_711 (m n : \u2115) (h\u2080 : 0 < m \u2227 0 < n) (h\u2081 : Nat.gcd m n = 8)\n (h\u2082 : Nat.lcm m n = 112) : 72 \u2264 m + n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2020_p22", "statement": "theorem amc12b_2020_p22 (t : \u211d) : (2 ^ t - 3 * t) * t / 4 ^ t \u2264 1 / 12", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_113", "statement": "theorem mathd_algebra_113 (x : \u211d) : x ^ 2 - 14 * x + 3 \u2265 7 ^ 2 - 14 * 7 + 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2020_p9", "statement": "theorem amc12a_2020_p9 (S : Finset \u211d)\n (h\u2080 : \u2200 x : \u211d, x \u2208 S \u2194 0 \u2264 x \u2227 x \u2264 2 * Real.pi \u2227 Real.tan (2 * x) = Real.cos (x / 2)) :\n S.card = 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12_2000_p1", "statement": "theorem amc12_2000_p1 (i m o : \u2115) (h\u2080 : i \u2260 m \u2227 m \u2260 o \u2227 o \u2260 i) (h\u2081 : i * m * o = 2001) :\n i + m + o \u2264 671", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2021_p19", "statement": "theorem amc12a_2021_p19 (S : Finset \u211d)\n (h\u2080 :\n \u2200 x : \u211d,\n x \u2208 S \u2194\n 0 \u2264 x \u2227\n x \u2264 Real.pi \u2227\n Real.sin (Real.pi / 2 * Real.cos x) = Real.cos (Real.pi / 2 * Real.sin x)) :\n S.card = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_amgm_sumasqdivbgeqsuma", "statement": "theorem algebra_amgm_sumasqdivbgeqsuma (a b c d : \u211d) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c \u2227 0 < d) :\n a ^ 2 / b + b ^ 2 / c + c ^ 2 / d + d ^ 2 / a \u2265 a + b + c + d", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_212", "statement": "theorem mathd_numbertheory_212 : 16 ^ 17 * 17 ^ 18 * 18 ^ 19 % 10 = 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_320", "statement": "theorem mathd_numbertheory_320 (n : \u2115) (h\u2080 : n < 101) (h\u2081 : 101 \u2223 123456 - n) : n = 34", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_125", "statement": "theorem mathd_algebra_125 (x y : \u2115) (h\u2080 : 0 < x \u2227 0 < y) (h\u2081 : 5 * x = y)\n (h\u2082 : \u2191x - (3 : \u2124) + (y - (3 : \u2124)) = 30) : x = 6", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "induction_1pxpownlt1pnx", "statement": "theorem induction_1pxpownlt1pnx (x : \u211d) (n : \u2115) (h\u2080 : -1 < x) (h\u2081 : 0 < n) :\n 1 + \u2191n * x \u2264 (1 + x) ^ (n : \u2115)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_148", "statement": "theorem mathd_algebra_148 (c : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = c * x ^ 3 - 9 * x + 3)\n (h\u2081 : f 2 = 9) : c = 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2019_p12", "statement": "theorem amc12a_2019_p12 (x y : \u211d) (h\u2080 : x \u2260 1 \u2227 y \u2260 1)\n (h\u2081 : Real.log x / Real.log 2 = Real.log 16 / Real.log y) (h\u2082 : x * y = 64) :\n (Real.log (x / y) / Real.log 2) ^ 2 = 20", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "induction_11div10tonmn1ton", "statement": "theorem induction_11div10tonmn1ton (n : \u2115) : 11 \u2223 10 ^ n - (-1 : \u2124) ^ n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_amgm_sum1toneqn_prod1tonleq1", "statement": "theorem algebra_amgm_sum1toneqn_prod1tonleq1 (a : \u2115 \u2192 NNReal) (n : \u2115)\n (h\u2080 : (\u2211 x in Finset.range n, a x) = n) : (\u220f x in Finset.range n, a x) \u2264 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1985_p6", "statement": "theorem imo_1985_p6 (f : \u2115 \u2192 NNReal \u2192 \u211d) (h\u2080 : \u2200 x, f 1 x = x)\n (h\u2081 : \u2200 x n, f (n + 1) x = f n x * (f n x + 1 / n)) :\n \u2203! a, \u2200 n, 0 < n \u2192 0 < f n a \u2227 f n a < f (n + 1) a \u2227 f (n + 1) a < 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2020_p15", "statement": "theorem amc12a_2020_p15 (a b : \u2102) (h\u2080 : a ^ 3 - 8 = 0) (h\u2081 : b ^ 3 - 8 * b ^ 2 - 8 * b + 64 = 0) :\n Complex.abs (a - b) \u2264 2 * Real.sqrt 21", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_332", "statement": "theorem mathd_algebra_332 (x y : \u211d) (h\u2080 : (x + y) / 2 = 7) (h\u2081 : Real.sqrt (x * y) = Real.sqrt 19) :\n x ^ 2 + y ^ 2 = 158", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_cubrtrp1oncubrtreq3_rcubp1onrcubeq5778", "statement": "theorem algebra_cubrtrp1oncubrtreq3_rcubp1onrcubeq5778 (r : \u211d)\n (h\u2080 : r ^ ((1 : \u211d) / 3) + 1 / r ^ ((1 : \u211d) / 3) = 3) : r ^ 3 + 1 / r ^ 3 = 5778", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_293", "statement": "theorem mathd_algebra_293 (x : NNReal) :\n Real.sqrt (60 * x) * Real.sqrt (12 * x) * Real.sqrt (63 * x) = 36 * x * Real.sqrt (35 * x)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_440", "statement": "theorem mathd_algebra_440 (x : \u211d) (h\u2080 : 3 / 2 / 3 = x / 10) : x = 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_254", "statement": "theorem mathd_numbertheory_254 : (239 + 174 + 83) % 10 = 6", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12_2000_p6", "statement": "theorem amc12_2000_p6 (p q : \u2115) (h\u2080 : Nat.Prime p \u2227 Nat.Prime q) (h\u2081 : 4 \u2264 p \u2227 p \u2264 18)\n (h\u2082 : 4 \u2264 q \u2227 q \u2264 18) : p * q - (p + q) \u2260 194", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1988_p8", "statement": "theorem aime_1988_p8 (f : \u2115 \u2192 \u2115 \u2192 \u211d) (h\u2080 : \u2200 x, 0 < x \u2192 f x x = x)\n (h\u2081 : \u2200 x y, 0 < x \u2227 0 < y \u2192 f x y = f y x)\n (h\u2082 : \u2200 x y, 0 < x \u2227 0 < y \u2192 (\u2191x + \u2191y) * f x y = y * f x (x + y)) : f 14 52 = 364", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_114", "statement": "theorem mathd_algebra_114 (a : \u211d) (h\u2080 : a = 8) :\n (16 * (a ^ 2) ^ ((1 : \u211d) / 3)) ^ ((1 : \u211d) / 3) = 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_2019_p1", "statement": "theorem imo_2019_p1 (f : \u2124 \u2192 \u2124) :\n (\u2200 a b, f (2 * a) + 2 * f b = f (f (a + b))) \u2194 \u2200 z, f z = 0 \u2228 \u2203 c, \u2200 z, f z = 2 * z + c", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_513", "statement": "theorem mathd_algebra_513 (a b : \u211d) (h\u2080 : 3 * a + 2 * b = 5) (h\u2081 : a + b = 2) : a = 1 \u2227 b = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_143", "statement": "theorem mathd_algebra_143 (f g : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = x + 1) (h\u2081 : \u2200 x, g x = x ^ 2 + 3) :\n f (g 2) = 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_354", "statement": "theorem mathd_algebra_354 (a d : \u211d) (h\u2080 : a + 6 * d = 30) (h\u2081 : a + 10 * d = 60) :\n a + 20 * d = 135", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1984_p7", "statement": "theorem aime_1984_p7 (f : \u2124 \u2192 \u2124) (h\u2080 : \u2200 n, 1000 \u2264 n \u2192 f n = n - 3)\n (h\u2081 : \u2200 n, n < 1000 \u2192 f n = f (f (n + 5))) : f 84 = 997", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_246", "statement": "theorem mathd_algebra_246 (a b : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 x, f x = a * x ^ 4 - b * x ^ 2 + x + 5)\n (h\u2082 : f (-3) = 2) : f 3 = 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1983_p3", "statement": "theorem aime_1983_p3 (f : \u211d \u2192 \u211d)\n (h\u2080 : \u2200 x, f x = x ^ 2 + (18 * x + 30) - 2 * Real.sqrt (x ^ 2 + (18 * x + 45)))\n (h\u2081 : Fintype (f \u207b\u00b9' {0})) : (\u220f x in (f \u207b\u00b9' {0}).toFinset, x) = 20", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "numbertheory_3pow2pownm1mod2pownp3eq2pownp2", "statement": "theorem numbertheory_3pow2pownm1mod2pownp3eq2pownp2 (n : \u2115) (h\u2080 : 0 < n) :\n (3 ^ 2 ^ n - 1) % 2 ^ (n + 3) = 2 ^ (n + 2)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_85", "statement": "theorem mathd_numbertheory_85 : 1 * 3 ^ 3 + 2 * 3 ^ 2 + 2 * 3 + 2 = 53", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12_2001_p21", "statement": "theorem amc12_2001_p21 (a b c d : \u2115) (h\u2080 : a * b * c * d = 8!) (h\u2081 : a * b + a + b = 524)\n (h\u2082 : b * c + b + c = 146) (h\u2083 : c * d + c + d = 104) : \u2191a - \u2191d = (10 : \u2124)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_239", "statement": "theorem mathd_numbertheory_239 : (\u2211 k in Finset.Icc 1 12, k) % 4 = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2002_p2", "statement": "theorem amc12b_2002_p2 (x : \u2124) (h\u2080 : x = 4) :\n (3 * x - 2) * (4 * x + 1) - (3 * x - 2) * (4 * x) + 1 = 11", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_196", "statement": "theorem mathd_algebra_196 (S : Finset \u211d) (h\u2080 : \u2200 x : \u211d, x \u2208 S \u2194 abs (2 - x) = 3) :\n (\u2211 k in S, k) = 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_342", "statement": "theorem mathd_algebra_342 (a d : \u211d) (h\u2080 : (\u2211 k in Finset.range 5, a + k * d) = 70)\n (h\u2081 : (\u2211 k in Finset.range 10, a + k * d) = 210) : a = 42 / 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_517", "statement": "theorem mathd_numbertheory_517 : 121 * 122 * 123 % 4 = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2009_p7", "statement": "theorem amc12a_2009_p7 (x : \u211d) (n : \u2115) (a : \u2115 \u2192 \u211d)\n (h\u2081 : \u2200 m, a (m + 1) - a m = a (m + 2) - a (m + 1)) (h\u2082 : a 1 = 2 * x - 3)\n (h\u2083 : a 2 = 5 * x - 11) (h\u2084 : a 3 = 3 * x + 1) (h\u2085 : a n = 2009) : n = 502", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_270", "statement": "theorem mathd_algebra_270 (f : \u211d \u2192 \u211d) (h\u2080 : \u2200 (x) (_ : x \u2260 -2), f x = 1 / (x + 2)) :\n f (f 1) = 3 / 7", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2021_p12", "statement": "theorem amc12a_2021_p12 (a b c d : \u211d) (f : \u2102 \u2192 \u2102)\n (h\u2080 : \u2200 z, f z = z ^ 6 - 10 * z ^ 5 + a * z ^ 4 + b * z ^ 3 + c * z ^ 2 + d * z + 16)\n (h\u2081 : \u2200 z, f z = 0 \u2192 z.im = 0 \u2227 0 < z.re \u2227 \u2191(Int.floor z.re) = z.re) : b = -88", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_362", "statement": "theorem mathd_algebra_362 (a b : \u211d) (h\u2080 : a ^ 2 * b ^ 3 = 32 / 27) (h\u2081 : a / b ^ 3 = 27 / 4) :\n a + b = 8 / 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_521", "statement": "theorem mathd_numbertheory_521 (m n : \u2115) (h\u2080 : Even m) (h\u2081 : Even n) (h\u2082 : m - n = 2)\n (h\u2083 : m * n = 288) : m = 18", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2002_p13", "statement": "theorem amc12a_2002_p13 (a b : \u211d) (h\u2080 : 0 < a \u2227 0 < b) (h\u2081 : a \u2260 b) (h\u2082 : abs (a - 1 / a) = 1)\n (h\u2083 : abs (b - 1 / b) = 1) : a + b = Real.sqrt 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1964_p2", "statement": "theorem imo_1964_p2 (a b c : \u211d) (h\u2080 : 0 < a \u2227 0 < b \u2227 0 < c) (h\u2081 : c < a + b) (h\u2082 : b < a + c)\n (h\u2083 : a < b + c) :\n a ^ 2 * (b + c - a) + b ^ 2 * (c + a - b) + c ^ 2 * (a + b - c) \u2264 3 * a * b * c", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_289", "statement": "theorem mathd_algebra_289 (k t m n : \u2115) (h\u2080 : Nat.Prime m \u2227 Nat.Prime n) (h\u2081 : t < k)\n (h\u2082 : k ^ 2 - m * k + n = 0) (h\u2083 : t ^ 2 - m * t + n = 0) :\n m ^ n + n ^ m + k ^ t + t ^ k = 20", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2021_p3", "statement": "theorem amc12a_2021_p3 (x y : \u2115) (h\u2080 : x + y = 17402) (h\u2081 : 10 \u2223 x) (h\u2082 : x / 10 = y) :\n \u2191x - \u2191y = (14238 : \u2124)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2008_p25", "statement": "theorem amc12a_2008_p25 (a b : \u2115 \u2192 \u211d) (h\u2080 : \u2200 n, a (n + 1) = Real.sqrt 3 * a n - b n)\n (h\u2081 : \u2200 n, b (n + 1) = Real.sqrt 3 * b n + a n) (h\u2082 : a 100 = 2) (h\u2083 : b 100 = 4) :\n a 1 + b 1 = 1 / 2 ^ 98", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_apbpceq2_abpbcpcaeq1_aleq1on3anbleq1ancleq4on3", "statement": "theorem algebra_apbpceq2_abpbcpcaeq1_aleq1on3anbleq1ancleq4on3 (a b c : \u211d) (h\u2080 : a \u2264 b \u2227 b \u2264 c)\n (h\u2081 : a + b + c = 2) (h\u2082 : a * b + b * c + c * a = 1) :\n 0 \u2264 a \u2227 a \u2264 1 / 3 \u2227 1 / 3 \u2264 b \u2227 b \u2264 1 \u2227 1 \u2264 c \u2227 c \u2264 4 / 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_66", "statement": "theorem mathd_numbertheory_66 : 194 % 11 = 7", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2021_p1", "statement": "theorem amc12b_2021_p1 (S : Finset \u2124) (h\u2080 : \u2200 x : \u2124, x \u2208 S \u2194 \u2191(abs x) < 3 * Real.pi) :\n S.card = 19", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_apbon2pownleqapownpbpowon2", "statement": "theorem algebra_apbon2pownleqapownpbpowon2 (a b : \u211d) (n : \u2115) (h\u2080 : 0 < a \u2227 0 < b) (h\u2081 : 0 < n) :\n ((a + b) / 2) ^ n \u2264 (a ^ n + b ^ n) / 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1968_p5_1", "statement": "theorem imo_1968_p5_1 (a : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : 0 < a)\n (h\u2081 : \u2200 x, f (x + a) = 1 / 2 + Real.sqrt (f x - f x ^ 2)) : \u2203 b > 0, \u2200 x, f (x + b) = f x", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1990_p15", "statement": "theorem aime_1990_p15 (a b x y : \u211d) (h\u2080 : a * x + b * y = 3) (h\u2081 : a * x ^ 2 + b * y ^ 2 = 7)\n (h\u2082 : a * x ^ 3 + b * y ^ 3 = 16) (h\u2083 : a * x ^ 4 + b * y ^ 4 = 42) :\n a * x ^ 5 + b * y ^ 5 = 20", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_235", "statement": "theorem mathd_numbertheory_235 : (29 * 79 + 31 * 81) % 10 = 2", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2020_p13", "statement": "theorem amc12b_2020_p13 :\n Real.sqrt (Real.log 6 / Real.log 2 + Real.log 6 / Real.log 3) =\n Real.sqrt (Real.log 3 / Real.log 2) + Real.sqrt (Real.log 2 / Real.log 3)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12b_2021_p13", "statement": "theorem amc12b_2021_p13 (S : Finset \u211d)\n (h\u2080 :\n \u2200 x : \u211d, x \u2208 S \u2194 0 < x \u2227 x \u2264 2 * Real.pi \u2227 1 - 3 * Real.sin x + 5 * Real.cos (3 * x) = 0) :\n S.card = 6", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_234", "statement": "theorem mathd_numbertheory_234 (a b : \u2115) (h\u2080 : 1 \u2264 a \u2227 a \u2264 9 \u2227 b \u2264 9)\n (h\u2081 : (10 * a + b) ^ 3 = 912673) : a + b = 16", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "numbertheory_aoddbdiv4asqpbsqmod8eq1", "statement": "theorem numbertheory_aoddbdiv4asqpbsqmod8eq1 (a : \u2124) (b : \u2115) (h\u2080 : Odd a) (h\u2081 : 4 \u2223 b) :\n (a ^ 2 + (b ^ 2 : \u2115)) % 8 = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_222", "statement": "theorem mathd_numbertheory_222 (b : \u2115) (h\u2080 : Nat.lcm 120 b = 3720) (h\u2081 : Nat.gcd 120 b = 8) :\n b = 248", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1999_p11", "statement": "theorem aime_1999_p11 (m : \u211a) (h\u2080 : 0 < m)\n (h\u2081 : (\u2211 k in Finset.Icc (1 : \u2115) 35, Real.sin (5 * k * \u03c0 / 180)) = Real.tan (m * \u03c0 / 180))\n (h\u2082 : (m.num : \u211d) / m.den < 90) : \u2191m.den + m.num = 177", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_359", "statement": "theorem mathd_algebra_359 (y : \u211d) (h\u2080 : y + 6 + y = 2 * 12) : y = 9", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1965_p2", "statement": "theorem imo_1965_p2 (x y z : \u211d) (a : \u2115 \u2192 \u211d) (h\u2080 : 0 < a 0 \u2227 0 < a 4 \u2227 0 < a 8)\n (h\u2081 : a 1 < 0 \u2227 a 2 < 0) (h\u2082 : a 3 < 0 \u2227 a 5 < 0) (h\u2083 : a 6 < 0 \u2227 a 7 < 0)\n (h\u2084 : 0 < a 0 + a 1 + a 2) (h\u2085 : 0 < a 3 + a 4 + a 5) (h\u2086 : 0 < a 6 + a 7 + a 8)\n (h\u2087 : a 0 * x + a 1 * y + a 2 * z = 0) (h\u2088 : a 3 * x + a 4 * y + a 5 * z = 0)\n (h\u2089 : a 6 * x + a 7 * y + a 8 * z = 0) : x = 0 \u2227 y = 0 \u2227 z = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_288", "statement": "theorem mathd_algebra_288 (x y : \u211d) (n : NNReal) (h\u2080 : x < 0 \u2227 y < 0) (h\u2081 : abs y = 6)\n (h\u2082 : Real.sqrt ((x - 8) ^ 2 + (y - 3) ^ 2) = 15)\n (h\u2083 : Real.sqrt (x ^ 2 + y ^ 2) = Real.sqrt n) : n = 52", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_127", "statement": "theorem mathd_numbertheory_127 : (\u2211 k in Finset.range 101, 2 ^ k) % 7 = 3", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "imo_1974_p3", "statement": "theorem imo_1974_p3 (n : \u2115) :\n \u00ac5 \u2223 \u2211 k in Finset.range (n + 1), Nat.choose (2 * n + 1) (2 * k + 1) * 2 ^ (3 * k)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1991_p9", "statement": "theorem aime_1991_p9 (x : \u211d) (m : \u211a) (h\u2080 : 1 / Real.cos x + Real.tan x = 22 / 7)\n (h\u2081 : 1 / Real.sin x + 1 / Real.tan x = m) : \u2191m.den + m.num = 44", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2009_p6", "statement": "theorem amc12a_2009_p6 (m n p q : \u211d) (h\u2080 : p = 2 ^ m) (h\u2081 : q = 3 ^ n) :\n p ^ (2 * n) * q ^ m = 12 ^ (m * n)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_158", "statement": "theorem mathd_algebra_158 (a : \u2115) (h\u2080 : Even a)\n (h\u2081 : \u2191(\u2211 k in Finset.range 8, 2 * k + 1) - \u2191(\u2211 k in Finset.range 5, a + 2 * k) = (4 : \u2124)) :\n a = 8", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "algebra_absxm1pabsxpabsxp1eqxp2_0leqxleq1", "statement": "theorem algebra_absxm1pabsxpabsxp1eqxp2_0leqxleq1 (x : \u211d)\n (h\u2080 : abs (x - 1) + abs x + abs (x + 1) = x + 2) : 0 \u2264 x \u2227 x \u2264 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1990_p4", "statement": "theorem aime_1990_p4 (x : \u211d) (h\u2080 : 0 < x) (h\u2081 : x ^ 2 - 10 * x - 29 \u2260 0)\n (h\u2082 : x ^ 2 - 10 * x - 45 \u2260 0) (h\u2083 : x ^ 2 - 10 * x - 69 \u2260 0)\n (h\u2084 : 1 / (x ^ 2 - 10 * x - 29) + 1 / (x ^ 2 - 10 * x - 45) - 2 / (x ^ 2 - 10 * x - 69) = 0) :\n x = 13", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_541", "statement": "theorem mathd_numbertheory_541 (m n : \u2115) (h\u2080 : 1 < m) (h\u2081 : 1 < n) (h\u2082 : m * n = 2005) :\n m + n = 406", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_314", "statement": "theorem mathd_algebra_314 (n : \u2115) (h\u2080 : n = 11) : (1 / 4) ^ (n + 1) * 2 ^ (2 * n) = 1 / 4", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12_2000_p20", "statement": "theorem amc12_2000_p20 (x y z : \u211d) (h\u2080 : 0 < x \u2227 0 < y \u2227 0 < z) (h\u2081 : x + 1 / y = 4)\n (h\u2082 : y + 1 / z = 1) (h\u2083 : z + 1 / x = 7 / 3) : x * y * z = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_302", "statement": "theorem mathd_algebra_302 : (Complex.I / 2) ^ 2 = -(1 / 4)", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1983_p2", "statement": "theorem aime_1983_p2 (x p : \u211d) (f : \u211d \u2192 \u211d) (h\u2080 : 0 < p \u2227 p < 15) (h\u2081 : p \u2264 x \u2227 x \u2264 15)\n (h\u2082 : f x = abs (x - p) + abs (x - 15) + abs (x - p - 15)) : 15 \u2264 f x", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_139", "statement": "theorem mathd_algebra_139 (s : \u211d \u2192 \u211d \u2192 \u211d)\n (h\u2080 : \u2200 (x) (_ : x \u2260 0), \u2200 (y) (_ : y \u2260 0), s x y = (1 / y - 1 / x) / (x - y)) :\n s 3 11 = 1 / 33", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2021_p25", "statement": "theorem amc12a_2021_p25 (N : \u2115) (f : \u2115 \u2192 \u211d)\n (h\u2080 : \u2200 n, 0 < n \u2192 f n = (Nat.divisors n).card / n ^ ((1 : \u211d) / 3))\n (h\u2081 : \u2200 (n) (_ : n \u2260 N), 0 < n \u2192 f n < f N) : (Nat.digits 10 N).sum = 9", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "amc12a_2020_p25", "statement": "theorem amc12a_2020_p25 (a : \u211a) (S : Finset \u211d)\n (h\u2080 : \u2200 x : \u211d, x \u2208 S \u2194 \u2191\u230ax\u230b * (x - \u2191\u230ax\u230b) = \u2191a * x ^ 2) (h\u2081 : (\u2211 k in S, k) = 420) :\n \u2191a.den + a.num = 929", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_150", "statement": "theorem mathd_numbertheory_150 (n : \u2115) (h\u2080 : \u00acNat.Prime (7 + 30 * n)) : 6 \u2264 n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1989_p8", "statement": "theorem aime_1989_p8 (a b c d e f g : \u211d)\n (h\u2080 : a + 4 * b + 9 * c + 16 * d + 25 * e + 36 * f + 49 * g = 1)\n (h\u2081 : 4 * a + 9 * b + 16 * c + 25 * d + 36 * e + 49 * f + 64 * g = 12)\n (h\u2082 : 9 * a + 16 * b + 25 * c + 36 * d + 49 * e + 64 * f + 81 * g = 123) :\n 16 * a + 25 * b + 36 * c + 49 * d + 64 * e + 81 * f + 100 * g = 334", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_296", "statement": "theorem mathd_numbertheory_296 (n : \u2115) (h\u2080 : 2 \u2264 n) (h\u2081 : \u2203 x, x ^ 3 = n) (h\u2082 : \u2203 t, t ^ 4 = n) :\n 4096 \u2264 n", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_142", "statement": "theorem mathd_algebra_142 (m b : \u211d) (h\u2080 : m * 7 + b = -1) (h\u2081 : m * -1 + b = 7) : m + b = 5", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "numbertheory_exk2powkeqapb2mulbpa2_aeq1", "statement": "theorem numbertheory_exk2powkeqapb2mulbpa2_aeq1 (a b : \u2115) (h\u2080 : 0 < a \u2227 0 < b)\n (h\u2081 : \u2203 k > 0, 2 ^ k = (a + b ^ 2) * (b + a ^ 2)) : a = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_400", "statement": "theorem mathd_algebra_400 (x : \u211d) (h\u2080 : 5 + 500 / 100 * 10 = 110 / 100 * x) : x = 50", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "aime_1995_p7", "statement": "theorem aime_1995_p7 (k m n : \u2115) (t : \u211d) (h\u2080 : 0 < k \u2227 0 < m \u2227 0 < n) (h\u2081 : Nat.gcd m n = 1)\n (h\u2082 : (1 + Real.sin t) * (1 + Real.cos t) = 5 / 4)\n (h\u2083 : (1 - Real.sin t) * (1 - Real.cos t) = m / n - Real.sqrt k) : k + m + n = 27", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_185", "statement": "theorem mathd_numbertheory_185 (n : \u2115) (h\u2080 : n % 5 = 3) : 2 * n % 5 = 1", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_441", "statement": "theorem mathd_algebra_441 (x : \u211d) (h\u2080 : x \u2260 0) :\n 12 / (x * x) * (x ^ 4 / (14 * x)) * (35 / (3 * x)) = 10", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_numbertheory_582", "statement": "theorem mathd_numbertheory_582 (n : \u2115) (h\u2080 : 0 < n) (h\u2081 : 3 \u2223 n) :\n (n + 4 + (n + 6) + (n + 8)) % 9 = 0", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} +{"full_name": "mathd_algebra_338", "statement": "theorem mathd_algebra_338 (a b c : \u211d) (h\u2080 : 3 * a + b + c = -3) (h\u2081 : a + 3 * b + c = 9)\n (h\u2082 : a + b + 3 * c = 19) : a * b * c = -56", "url": "https://github.com/rah4927/lean-dojo-mew", "commit": "d00c776260c77de7e70125ef0cd119de6c0ff1de", "file_path": "MiniF2F/Test.lean", "split": "test"} diff --git a/data/test.jsonl b/data/test.jsonl new file mode 100644 index 0000000..de02c68 --- /dev/null +++ b/data/test.jsonl @@ -0,0 +1,2 @@ +{"full_name": "testing1", "statement": "∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b", "file_path": "None"} +{"full_name": "testing2", "statement": "forall (p q: Prop), Or p q -> Or q p", "file_path": "None"} \ No newline at end of file From 8e4b4f916388a362950b191027b3e62980258229 Mon Sep 17 00:00:00 2001 From: Sai Konkimalla Date: Thu, 30 May 2024 12:59:49 -0700 Subject: [PATCH 3/3] Added output of proof search function on test dataset --- .../test/30-05-2024-12-29/logs/testing1.txt | 49 +++++++++++++ .../test/30-05-2024-12-29/logs/testing2.txt | 69 +++++++++++++++++++ .../results__gpt-3.5-turbo__0.json | 54 +++++++++++++++ 3 files changed, 172 insertions(+) create mode 100644 output/test/30-05-2024-12-29/logs/testing1.txt create mode 100644 output/test/30-05-2024-12-29/logs/testing2.txt create mode 100644 output/test/30-05-2024-12-29/results__gpt-3.5-turbo__0.json diff --git a/output/test/30-05-2024-12-29/logs/testing1.txt b/output/test/30-05-2024-12-29/logs/testing1.txt new file mode 100644 index 0000000..290a771 --- /dev/null +++ b/output/test/30-05-2024-12-29/logs/testing1.txt @@ -0,0 +1,49 @@ +Theorem number: 1 + +Initial state: +⊢ ∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b + +--------------------------- +Iteration 1 +--------------------------- + +Tactic candidates: +['intros a b h'] + +Tactic scores (-log prob): +[0.30103418611] + +Tactic 1 result: not solved +a : Nat +b : Nat +h : b = 2 +⊢ 1 + a + 1 = a + b + +--------------------------- +Iteration 2 +--------------------------- + +Tactic candidates: +['rw [h]'] + +Tactic scores (-log prob): +[0.0892465625] + +Tactic 1 result: not solved +a : Nat +b : Nat +h : b = 2 +⊢ 1 + a + 1 = a + 2 + +--------------------------- +Iteration 3 +--------------------------- + +Tactic candidates: +['rw [h]'] + +Tactic scores (-log prob): +[0.2368663525] + +Theorem error +Failure reason: ServerError ["tactic 'rewrite' failed, did not find instance of the pattern in the target expression\n b\na b : Nat\nh : b = 2\n⊢ 1 + a + 1 = a + 2"] \ No newline at end of file diff --git a/output/test/30-05-2024-12-29/logs/testing2.txt b/output/test/30-05-2024-12-29/logs/testing2.txt new file mode 100644 index 0000000..4599f20 --- /dev/null +++ b/output/test/30-05-2024-12-29/logs/testing2.txt @@ -0,0 +1,69 @@ +Theorem number: 2 + +Initial state: +⊢ forall (p q: Prop), Or p q -> Or q p + +--------------------------- +Iteration 1 +--------------------------- + +Tactic candidates: +['intros p q h'] + +Tactic scores (-log prob): +[0.217274595475] + +Tactic 1 result: not solved +p : Prop +q : Prop +h : p ∨ q +⊢ q ∨ p + +--------------------------- +Iteration 2 +--------------------------- + +Tactic candidates: +['cases h'] + +Tactic scores (-log prob): +[0.06462308351666667] + +Tactic 1 result: not solved +p : Prop +q : Prop +h✝ : p +⊢ q ∨ p +p : Prop +q : Prop +h✝ : q +⊢ q ∨ p + +--------------------------- +Iteration 3 +--------------------------- + +Tactic candidates: +['left'] + +Tactic scores (-log prob): +[0.602736965] + +Tactic 1 result: not solved +p : Prop +q : Prop +h✝ : p +⊢ q + +--------------------------- +Iteration 4 +--------------------------- + +Tactic candidates: +['exact h\\xe2\\x9c\\x9d'] + +Tactic scores (-log prob): +[0.00540535255116] + +Theorem error +Failure reason: ServerError :1:11: expected end of input \ No newline at end of file diff --git a/output/test/30-05-2024-12-29/results__gpt-3.5-turbo__0.json b/output/test/30-05-2024-12-29/results__gpt-3.5-turbo__0.json new file mode 100644 index 0000000..5a12a4c --- /dev/null +++ b/output/test/30-05-2024-12-29/results__gpt-3.5-turbo__0.json @@ -0,0 +1,54 @@ +{ + "results": [ + { + "attempt_results": [ + { + "theorem": "\u2200 (a b: Nat), (b = 2) -> 1 + a + 1 = a + b", + "success": false, + "failure_reason": "ServerError" + } + ], + "success": false, + "example": { + "full_name": "testing1", + "statement": "\u2200 (a b: Nat), (b = 2) -> 1 + a + 1 = a + b", + "file_path": "None" + } + }, + { + "attempt_results": [ + { + "theorem": "forall (p q: Prop), Or p q -> Or q p", + "success": false, + "failure_reason": "ServerError" + } + ], + "success": false, + "example": { + "full_name": "testing2", + "statement": "forall (p q: Prop), Or p q -> Or q p", + "file_path": "None" + } + } + ], + "args": { + "model_name": "gpt-3.5-turbo", + "dataset_name": "test-set", + "shard": 0, + "resume_from": null, + "dataset_path": "data/test.jsonl", + "output_dir": "output/test", + "early_stop": false, + "tp_degree": 1, + "num_shards": 8, + "max_iters": 5, + "timeout": 600, + "num_examples": -1, + "num_samples": 1, + "clear_process_hours": 3, + "temperatures": [ + 0.0 + ], + "api_key_path": "../api_key/key.txt" + } +} \ No newline at end of file