ଦାବିକୁ ଦର୍ଶାନ୍ତୁ। କର୍ଣ୍ଣେଲ ଏହା ପ୍ରମାଣିତ ହୋଇଛି କି ନାହିଁ ତାହା ନିର୍ଦ୍ଧାରଣ କରେ।

ଗୋଟିଏ ପ୍ୟାନେଲର ମଡେଲ ଆପଣଙ୍କର ସମସ୍ୟାକୁ ସାହିତ୍ୟ, SageMath, PARI/GP ଏବଂ SMT ସମାଧାନକାରୀ ସହିତ ଆକ୍ରମଣ କରେ, ତାପରେ Lean 4ରେ Mathlib ବିରୁଦ୍ଧରେ ଫଳାଫଳକୁ ଆଇନଗତ କରେ। ଲିନ'ସ କାର୍ନେଲ ପ୍ରମାଣକୁ ଗ୍ରହଣ କରେ କିମ୍ବା ଏହା କରେ ନାହିଁ, ଏବଂ କୌଣସି ପରିମାଣର ବିଶ୍ୱାସଯୋଗ୍ୟ ପ୍ରବନ୍ଧ ତାହାକୁ ପରିବର୍ତ୍ତନ କରେ ନାହିଁ। ଯେତେବେଳେ ଏହା ବିଫଳ ହୋଇଥାଏ, ଆପଣ ଠିକ ଲକ୍ଷ୍ୟ ପାଇବେ ଯାହାକି ବସିଥାଏ, ଯାହା ସାଧାରଣତଃ ଅଣ-ଅନୁସୂଚିତ ତର୍କ ହସ୍ତ-ବଲବଲ କରିବା ସମୟରେ ଥାଏ।

ଲକ୍ଷ୍ୟ
ଶେଷ ହୋଇଥିବା ବିଷୟରେ ନିର୍ଦ୍ଦିଷ୍ଟ ହୁଅନ୍ତୁ ଯାହାର ଅର୍ଥ ହେଉଛି. 'X ସତ କି ନାହିଁ ତାହା ନିର୍ଣ୍ଣୟ କରନ୍ତୁ, ଏବଂ ଏହାକୁ ପ୍ରମାଣିତ କରନ୍ତୁ' 'X ବିଷୟରେ ମୋତେ କୁହନ୍ତୁ' କୁ ହାର ମାରୁଛି।
ପଟି ଯାହାକୁ ସଫାକରିବାକୁ ହେବ
ରେଫରି ଏହି ବାରକୁ ବାସ୍ତବରେ ଧରିଥାଏ। ପୁରସ୍କାର ସ୍ତର ପ୍ରମାଣ ପାଇଁ ପଚାରନ୍ତୁ ଏବଂ ଏହା ଆପଣଙ୍କୁ ସ୍ପଷ୍ଟ ଭାବରେ କହିବ ଯେପରି ପ୍ୟାନେଲ ଛୋଟ ହୋଇଯାଏ, ବିଜୟ ଘୋଷଣା କରିବା ବଦଳରେ।
ଫଳକ
ଅଧିକ ସିଟ ଅର୍ଥ ଅଧିକ ଆଙ୍ଗୁଳି ଏବଂ ପ୍ରତି ରାଉଣ୍ଡରେ ଅଧିକ ଖର୍ଚ୍ଚ ।
ରେଫରି
ମାପକାଠି ଉପରେ ନିୟମ ଏବଂ ପ୍ରତ୍ୟେକ ପ୍ରମାଣକୁ ପୁନଃ ଯାଞ୍ଚ କରନ୍ତୁ । ଆପଣଙ୍କର ସବୁଠୁ ଶକ୍ତିଶାଳୀ ମଡେଲର ମୂଲ୍ୟ ।
ରାଉଣ୍ଡ
ଖର୍ଚ୍ଚ ସୀମା
Hitting it pauses the match. Nothing is lost.
ଦୃଶ୍ୟମାନତା
match ଆରମ୍ଭ କରିବା ପାଇଁ ସଦସ୍ୟତା ନିଅନ୍ତୁ
New accounts get starting credit, enough for a real match.
ଗୋଟିଏ ଯାଞ୍ଚକାରୀ ଯାହାକି ନିଶ୍ଚିତ କରାଯାଇପାରିବ ନାହିଁ

Lean 4 Mathlib ସହିତ ଅନ୍ତିମ ବକ୍ତବ୍ୟକୁ ଟାଇପ-ପରୀକ୍ଷଣ କରେ, ଏବଂ ଗୋଟିଏ ପ୍ରମାଣ ଯାହାକି sorry, native_decide କିମ୍ବା ଗୋଟିଏ ନୂତନ ଅକ୍ଷୟ ଉପରେ ଧାରଣ କରିଥାଏ ତାହାକୁ ଗଣନା କରିବା ବଦଳରେ ପ୍ରତ୍ୟାଖ୍ୟାନ କରାଯାଏ। ଏହା ସହିତ: SageMath, PARI/GP, Z3, CVC5 ଏବଂ OEIS, ତେଣୁ ଗୋଟିଏ ନିର୍ମାଣକୁ ଗଣନା କରାଯାଇପାରିବ ଏବଂ ଚିହ୍ନଟ କରାଯାଇପାରିବ ଯେପରି କେହି ଏହା ବିଷୟରେ କିଛି ପ୍ରମାଣିତ କରିବାକୁ ଚେଷ୍ଟା କରନ୍ତି।

ଗୋଟିଏ ବିଫଳ ପ୍ରମାଣ ଏକ ସନ୍ଧାନ

ଯେତେବେଳେ ଔପଚାରିକ ବିଫଳ ହୁଏ, ଲକ୍ଷ୍ୟ ଲିନ ବନ୍ଦ କରିପାରିଲା ନାହିଁ ତାହାକୁ ଆକ୍ରମଣ କରିବା ପାଇଁ ସବୁଠାରୁ ଭଲ ସ୍ଥାନକୁ ଦିଆଯାଏ: କେବଳ ସେହି ଲକ୍ଷ୍ୟ, ସମ୍ପୂର୍ଣ୍ଣ ଇତିହାସ ନୁହେଁ। ଗୋଟିଏ ପ୍ରତ୍ୟାଖ୍ୟାନ ପ୍ରମାଣଟି ଅନ୍ତରକୁ ସଠିକ ଭାବରେ ନାମକରଣ କରେ, ଯାହାକି ଅଧିକାଂଶ ଅନୌପଚାରିକ ତର୍କର ତୁଳନାରେ ଅଧିକ।

କିଛି ବି ଦୁଇଥର ପ୍ରମାଣିତ ହୋଇନଥାଏ

ପ୍ରତ୍ୟେକ ଲେମା ପ୍ୟାନେଲ ପ୍ରତିଷ୍ଠା କରିଥାଏ ତାହାର ପ୍ରମାଣ ସହିତ ଗୋଟିଏ ସହଭାଗୀ ଲଗରେ ଯାଏ, ତେଣୁ ଏହା କେବେବି ପୁନଃ ନିର୍ଗତ ହୋଇନଥାଏ ଏବଂ ଅଚଳ ଶେଷକୁ କେବେବି ପୁନଃପ୍ରୟାସ କରାଯାଇନଥାଏ। ଦୀର୍ଘ ସମସ୍ୟାଗୁଡିକ କାର୍ଯ୍ୟ ହରାଇ ନଥିବା ବିରତି ଏବଂ ପୁନଃପ୍ରାପ୍ତ ହୁଏ: ଟ୍ୟାବକୁ ବନ୍ଦ କରନ୍ତୁ ଏବଂ ଆସନ୍ତାକାଲି ଫେରନ୍ତୁ।