ਦਾਅਵਾ ਦਿਓ । ਕਰਨਲ ਫੈਸਲਾ ਕਰੇਗਾ ਕਿ ਕੀ ਇਹ ਸਾਬਤ ਹੈ ।

ਮਾਡਲਾਂ ਦਾ ਇੱਕ ਪੈਨਲ ਤੁਹਾਡੀ ਸਮੱਸਿਆ ਉੱਤੇ ਸਾਹਿਤ, SageMath, PARI/GP ਅਤੇ SMT ਸੋਲਵਰ ਨਾਲ ਹਮਲਾ ਕਰਦਾ ਹੈ, ਫਿਰ Mathlib ਦੇ ਵਿਰੁੱਧ Lean 4 ਵਿੱਚ ਨਤੀਜਾ ਫਾਰਮੈਲੀਜ਼ ਕਰਦਾ ਹੈ । Lean ਦਾ ਕਰਨਲ ਜਾਂ ਤਾਂ ਸਬੂਤ ਨੂੰ ਸਵੀਕਾਰ ਕਰਦਾ ਹੈ ਜਾਂ ਨਹੀਂ, ਅਤੇ ਕੋਈ ਵੀ ਸੰਤੁਸ਼ਟ ਪਰਸੰਗ ਇਸ ਨੂੰ ਬਦਲਦਾ ਨਹੀਂ ਹੈ । ਜਦੋਂ ਇਹ ਅਸਫਲ ਹੁੰਦਾ ਹੈ ਤਾਂ ਤੁਹਾਨੂੰ ਸਹੀ ਟੀਚਾ ਮਿਲਦਾ ਹੈ, ਜੋ ਕਿ ਆਮ ਤੌਰ ਉੱਤੇ ਅਨਪੜ੍ਹ ਦਲੀਲ ਹੱਥ- ਵਗਾਉਣ ਵਾਲੀ ਹੁੰਦੀ ਹੈ ।

ਟੀਚਾ
ਕੀ ਕੀਤਾ ਦਾ ਮਤਲਬ ਹੈ, ਇਸ ਬਾਰੇ ਖਾਸ ਹੋ ਜਾਓ । 'ਫੈਸਲਾ ਕਰੋ ਕਿ X ਸੱਚ ਹੈ ਅਤੇ ਇਹ ਸਾਬਤ ਕਰੋ ਕਿ ਇਹ 'ਬੈਟ' 'ਤੇ ਹੈ, ਮੈਨੂੰ X ਬਾਰੇ ਦੱਸੋ ।
ਪੱਟੀ, ਜਿਸ ਨੂੰ ਸਾਫ਼ ਕਰਨਾ ਹੈ
ਰਿਫਰੀ ਇਸ ਪੱਟੀ ਨੂੰ ਸੱਚਮੁੱਚ ਹੀ ਫੜਦਾ ਹੈ। ਜੇਕਰ ਤੁਸੀਂ ਪੁਰਸਕਾਰ- ਪੱਧਰ ਦਾ ਸਬੂਤ ਮੰਗੇ ਤਾਂ ਇਹ ਤੁਹਾਨੂੰ ਦੱਸੇਗਾ ਕਿ ਪੈਨਲ ਕਿੰਨਾ ਛੋਟਾ ਹੈ, ਜਿੱਤ ਦਾ ਐਲਾਨ ਕਰਨ ਦੀ ਬਜਾਏ।
ਪੈਨਲ
ਵਧੇਰੇ ਸੀਟਾਂ ਦਾ ਅਰਥ ਹੈ ਵਧੇਰੇ ਕੋਣ ਅਤੇ ਪ੍ਰਤੀ ਗੇੜ ਵਧੇਰੇ ਲਾਗਤ।
ਰਿਫਰੈਸ਼ਰ
ਮਾਪਦੰਡਾਂ ਉੱਤੇ ਨਿਯਮ ਅਤੇ ਸਬੂਤ ਦੇ ਹਰੇਕ ਟੁਕੜੇ ਦੀ ਮੁੜ-ਚੈੱਕਿੰਗ। ਤੁਹਾਡੇ ਸਭ ਤੋਂ ਮਜ਼ਬੂਤ ਮਾਡਲ ਦੀ ਕੀਮਤ ਹੈ।
ਗੇੜ
ਖਰਚ ਲਿਮਟ
ਇਸ ਨੂੰ ਦਬਾਉਣ ਨਾਲ match ਵਿਰਾਮ ਹੋ ਜਾਵੇਗਾ । ਕੁਝ ਵੀ ਗੁਆਚ ਨਹੀਂ ਜਾਵੇਗਾ ।
ਦਿੱਖ
match ਸ਼ੁਰੂ ਕਰਨ ਲਈ ਸਾਈਨ ਅੱਪ ਕਰੋ
ਨਵੇਂ ਖਾਤੇ ਨੂੰ ਸ਼ੁਰੂਆਤੀ ਕਰੈਡਿਟ ਮਿਲਦਾ ਹੈ, ਜੋ ਕਿ ਅਸਲੀ match ਲਈ ਕਾਫੀ ਹੈ।
ਇੱਕ ਚੈਕਰ, ਜੋ ਕਿ ਮਨਜ਼ੂਰ ਨਹੀਂ ਕੀਤਾ ਜਾ ਸਕਦਾ ਹੈ

Mathlib ਨਾਲ Lean 4 ਫਾਈਨਲ ਸਟੇਟਮੈਂਟ ਦੀ ਕਿਸਮ- ਜਾਂਚ ਕਰਦਾ ਹੈ, ਅਤੇ ਇੱਕ ਪ੍ਰਮਾਣ ਜੋ ਕਿ sorry, native_decide ਜਾਂ ਇੱਕ ਤਾਜ਼ਾ ਐਕਸੀਓਮ ਉੱਤੇ ਅਧਾਰਿਤ ਹੈ, ਗਿਣਨ ਦੀ ਬਜਾਏ ਰੱਦ ਕੀਤਾ ਜਾਂਦਾ ਹੈ । ਇਸ ਦੇ ਨਾਲ: SageMath, PARI/GP, Z3, CVC5 ਅਤੇ OEIS, ਤਾਂ ਕਿ ਇੱਕ ਢਾਂਚਾ ਗਣਨਾ ਅਤੇ ਪਛਾਣ ਕੀਤਾ ਜਾ ਸਕੇ, ਜਦੋਂ ਤੱਕ ਕੋਈ ਇਸ ਬਾਰੇ ਕੁਝ ਵੀ ਸਾਬਤ ਕਰਨ ਦੀ ਕੋਸ਼ਿਸ ਨਹੀਂ ਕਰਦਾ ਹੈ ।

ਇੱਕ ਫੇਲ੍ਹ ਸਾਬਤ ਇੱਕ ਖੋਜ ਹੈ

ਜਦੋਂ ਫਾਰਮੈਲਿਜ਼ੇਸ਼ਨ ਫੇਲ੍ਹ ਹੋ ਜਾਵੇ ਤਾਂ ਟੀਚਾ Lean close ਨਹੀਂ ਕਰ ਸਕਦਾ ਹੈ, ਜਿਸ ਨੂੰ ਹਮਲੇ ਲਈ ਸਭ ਤੋਂ ਵਧੀਆ ਸਥਿਤੀ ਦਿੱਤੀ ਜਾਂਦੀ ਹੈ: ਸਿਰਫ ਇਹ ਟੀਚਾ, ਪੂਰੀ ਅਤੀਤ ਨਹੀਂ। ਇੱਕ ਰੱਦ ਕੀਤਾ ਸਾਬਤ ਗਲੀਚੇ ਦਾ ਨਾਂ ਸਹੀ ਹੈ, ਜੋ ਕਿ ਬਹੁਤੇ ਅਨਪੜ੍ਹ ਦਲੀਲ ਤੋਂ ਵੱਧ ਹੈ।

ਕੁਝ ਵੀ ਦੋ ਵਾਰ ਨਹੀਂ ਸਾਬਤ ਕੀਤਾ ਜਾਂਦਾ

ਹਰੇਕ ਲੀਮਾ, ਜੋ ਕਿ ਪੈਨਲ ਨੇ ਸਥਾਪਤ ਕੀਤਾ ਹੈ, ਇੱਕ ਸਾਂਝੇ ਲੇਜ਼ਰ ਵਿੱਚ ਆਪਣੇ ਪਰੂਫ ਨਾਲ ਜਾਂਦਾ ਹੈ, ਇਸ ਲਈ ਇਹ ਕਦੇ ਵੀ ਮੁੜ- ਪ੍ਰਾਪਤ ਨਹੀਂ ਕੀਤਾ ਜਾਂਦਾ ਹੈ ਅਤੇ ਬੇਅੰਤ ਅੰਤ ਕਦੇ ਵੀ ਮੁੜ- ਕੋਸ਼ਿਸ ਨਹੀਂ ਕੀਤਾ ਜਾਂਦਾ ਹੈ । ਲੰਬੇ ਸਮੱਸਿਆਵਾਂ ਨੂੰ ਕੰਮ ਗੁਆਉਣ ਤੋਂ ਬਿਨਾਂ ਵਿਰਾਮ ਅਤੇ ਮੁੜ- ਚਾਲੂ ਕੀਤਾ ਜਾਂਦਾ ਹੈ: ਟੈਬ ਬੰਦ ਕਰੋ ਅਤੇ ਕੱਲ੍ਹ ਮੁੜ ਆਓ ।