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