Luaigh an t-éileamh. Déanann an eithne cinneadh an bhfuil sé cruthaithe.

Ionsaíonn painéal samhlacha do fhadhb leis an litríocht, SageMath, PARI/GP agus réiteach SMT, ansin foirmíonn an toradh i Lean 4 i gcoinne Mathlib. Glacann eithne Lean leis an cruthúnas nó ní dhéanann sé, agus ní athraíonn aon mhéid próis muiníneach sin. Nuair a theipeann air faigheann tú an sprioc cruinn atá fágtha, agus is gnách go raibh an argóint neamhfhoirmiúil ag waving láimhe.

An sprioc

Bí sonrach faoi cad a chiallaíonn déanta. 'Cinneadh a dhéanamh an bhfuil X fíor, agus a chruthú go bhfuil sé' buille 'inis dom faoi X'.

An barra a bhfuil sé a ghlanadh

Careful expert

What a competent professional in the field would accept as done and correct.

Publication standard

Would survive peer review: every claim sourced or derived, methods stated, limitations acknowle…

Formal proof

A complete deductive argument. Every step justified, every assumption stated, no appeals to pla…

Prize standard

The bar a Clay Millennium Prize submission would face: a complete, self-contained, gap-free pro…

Decision-grade

Enough evidence to act on commercially: options costed, risks named, recommendation justified.

Write my own

Describe your own standard.

Iarr ar chruthúnas ar leibhéal duais agus inseoidh sé duit go soiléir nuair a thiteann an painéal gearr, seachas bua a dhearbhú.

An painéal

Ciallaíonn suíocháin níos mó uillinneacha níos mó, agus costas níos mó in aghaidh an bhabhta.

Réiteoir

Rialacha ar na critéir agus ath-seiceálacha gach píosa fianaise. Fiú do mhúnla is láidre.

Babhtaí

Teorainn chaiteachais

Má bhuaileann tú é, cuirfidh sé an cluiche ar shos. Níl aon rud caillte.

Infheictheacht

Foilsigh nuair atá sé críochnaithe

Cláraigh chun cluiche a thosú

Cuntais nua a fháil ag tosú creidmheasa, go leor le haghaidh cluiche fíor.

Seiceálaí nach féidir a chur ina luí air

Lean 4 le Mathlib cineál-seiceálacha an ráiteas deiridh, agus cruthúnas a leanings ar sorry, native_decide nó axiom úr a dhiúltú seachas a chomhaireamh.Taobh leis: SageMath, PARI/GP, Z3, CVC5 agus an OEIS, ionas gur féidir le tógáil a ríomh agus a aithint sula ndéanann duine ar bith iarracht rud ar bith a chruthú faoi.

Is fianaise é cruthúnas teipthe

Nuair a theipeann ar fhoirmiú, tugtar an sprioc nach bhféadfadh Lean a dhúnadh ar láimh don suíochán is fearr chun ionsaí a dhéanamh air: ach an sprioc sin, ní an stair ar fad.Ainmníonn cruthúnas diúltaithe an bhearna go beacht, rud atá níos mó ná an chuid is mó argóintí neamhfhoirmiúla a dhéanamh riamh.

Ní chruthaítear aon rud faoi dhó

Téann gach lemma a bhunaíonn an painéal i mórleabhar comhroinnte lena chruthúnas, mar sin ní dhéantar é a athdhíorthú agus ní dhéantar iarracht ar chríocha marbh. Fadhbanna fada sos agus a atosú gan obair a chailleadh: dún an cluaisín agus teacht ar ais amárach.