My problems
Signed in with GitHub, this page lists your roles, the words waiting for your approval on the problems you steward, and your open pull requests.
- erdos-1050 · gloss of the statement ·
whole· Draft - erdos-1050 · gloss of the witness ·
whole· Draft - erdos-1050 · explainer of the proof ·
overview· Draft - erdos-1050 · explainer of the proof ·
steps:s1· Draft - erdos-1050 · explainer of the proof ·
steps:hT,hroot· Draft - erdos-1050 · explainer of the proof ·
steps:hint,hq· Draft - erdos-1050 · explainer of the proof ·
steps:h0,hsmall,s7· Draft - erdos-1050 · explainer of the proof ·
steps:hnz,this· Draft - erdos-1050--h1 · gloss of the statement ·
whole· Draft - erdos-1050--h1-v2 · gloss of the statement ·
whole· Draft - erdos-1050--h1-v2 · gloss of the witness ·
whole· Draft - erdos-1050--h1-v2 · explainer of the proof ·
overview· Draft - erdos-1050--h1-v2 · explainer of the proof ·
steps:hrem_all.id1_full,hrem_all.id1_test,hrem_all.lower_test,hrem_all.rhs_test,hrem_all.upper_test· Draft - erdos-1050--h1-v2 · explainer of the proof ·
steps:hrem_all.lagr_eval,hrem_all.tail_coeff· Draft - erdos-1050--h1-v2 · explainer of the proof ·
steps:hrem_all.cauchy_fin,hrem_all.h4_series,hrem_all.split3T,hrem_all.tail3· Draft - erdos-1050--h1-v2 · explainer of the proof ·
steps:hrem_all.T_facts,hrem_all.h4_big,hrem_all.ineq_pow,hrem_all.nd_bound,hrem_all.prod_one_sub_ge· Draft - erdos-1050--h1-v2 · explainer of the proof ·
steps:hrem_all,hrem_all.e,hrem_all.hAq0,hrem_all.hAq1,hrem_all.hQx0,hrem_all.hQx1,hrem_all.s17· Draft - erdos-1050--h1-v2 · explainer of the proof ·
steps:s2,s3,s4· Draft - erdos-1050--h1-v2 · explainer of the proof ·
steps:hden,hrem· Draft - erdos-1050--h1-v2 · explainer of the proof ·
steps:key,pos· Draft - erdos-1050--h1-v2 · explainer of the proof ·
steps:bound,hsq,this· Draft - erdos-1050--h1-v2 · gloss of the partial ·
whole· Draft - erdos-1050--h1-v2--h1 · gloss of the statement ·
whole· Draft - erdos-1050--h1-v2--h1 · gloss of the witness ·
whole· Draft - erdos-1050--h1-v2--h2 · gloss of the statement ·
whole· Draft - erdos-1050--h1-v2--h2 · gloss of the witness ·
whole· Draft - erdos-1050--h1-v2--h2 · explainer of the proof ·
overview· Draft - erdos-1050--h1-v2--h2 · explainer of the proof ·
steps:h0,hV,hW,hdvd,hgeo,hpoly,hrec,hsumZ· Draft - erdos-1050--h1-v2--h2 · explainer of the proof ·
steps:numerator_integral,s10· Draft - erdos-1050--h1-v2--h2 · explainer of the proof ·
steps:hden,s12· Draft - erdos-1050--h1-v2--h2 · explainer of the proof ·
steps:hpf· Draft - erdos-1050--h1-v2--h2 · explainer of the proof ·
steps:hres· Draft - erdos-1050--h1-v2--h2--h1 · gloss of the statement ·
whole· Draft - erdos-1050--h1-v2--h2--h1 · gloss of the witness ·
whole· Draft - erdos-1050--h1-v2--h2--h1 · explainer of the proof ·
overview· Draft - erdos-1050--h1-v2--h2--h1 · explainer of the proof ·
steps:hsumZ· Draft - erdos-1050--h1-v2--h2--h1 · explainer of the proof ·
steps:h0,hV,hW,hrec· Draft - erdos-1050--h1-v2--h2--h1 · explainer of the proof ·
steps:hdvd,hgeo,hpoly· Draft - erdos-1050--h1-v2--h2--h1 · explainer of the proof ·
steps:residue_integral· Draft - erdos-1050--h1-v2--h2--h1 · explainer of the proof ·
steps:polypart_integral· Draft - erdos-1050--h1-v2--h2--h1 · explainer of the proof ·
steps:head_integral,s12· Draft - erdos-1050--h1-v2--h2--h1 · explainer of the proof ·
steps:hmer,s14· Draft - erdos-1050--h1-v2--h3 · gloss of the statement ·
whole· Draft - erdos-1050--h1-v2--h3 · gloss of the witness ·
whole· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
overview· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:id1_test,id1_test.s1,id1_test.s2,id1_test.s2.ih',id1_test.s2.s2,lower_test,lower_test.h1,lower_test.h1.hi',lower_test.this· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:rhs_test,rhs_test.e,rhs_test.h1,upper_test,upper_test.e,upper_test.h1· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:id1_full,id1_full.hG1,id1_full.hG2,id1_full.hPne,id1_full.hPne.this,id1_full.hR,id1_full.ha,id1_full.hdisj,id1_full.hexp,id1_full.hexp.s1,id1_full.hexp.s2,id1_full.hsign,id1_full.hsplit,id1_full.s7· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:lagr_eval,lagr_eval.hinj,lagr_eval.s2,lagr_eval.s2.s1,lagr_eval.s2.s2,lagr_eval.s2.s2.this,lagr_eval.s3,lagr_eval.s3.hk',lagr_eval.s3.hk'.this,lagr_eval.s3.s1,lagr_eval.s3.s3,lagr_eval.s3.s4,lagr_eval.s3.s5· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:deriv_prod_eval,deriv_prod_eval_node,deriv_prod_eval_node.s1,deriv_prod_eval_node.s2,lagr_deriv,lagr_deriv.hkmem,lagr_deriv.s2,lagr_deriv.s2.hjk,lagr_deriv.s3· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:formula3,formula3.hD,formula3.hD2,formula3.hNdeg,formula3.hNk,formula3.hNk',formula3.hPne,formula3.hkmem,formula3.hr,formula3.hxinj,formula3.hxinj.h',formula3.hxne· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:formula3.hD3,formula3.hD4,formula3.ha,formula3.ha.hne,formula3.hb,formula3.hb.hne,formula3.hc,formula3.hc.hKn,formula3.hc.hne,formula3.key,formula3.key.e1,formula3.key.e2,formula3.key.e3· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:formula3.hdisj,formula3.hhigh,formula3.hhigh.hkj,formula3.hhigh.hne,formula3.hhigh.hne.this,formula3.hhigh.hne2,formula3.hlow,formula3.hlow.hjk,formula3.hlow.hne,formula3.hlow.hne.this,formula3.hlow.hne2,formula3.hsplit,hform· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:gauss,gauss.hD,gauss.hD.h1,gauss.hDk,gauss.key,gauss.key.hDj,gauss.key.hj,gauss.key.hshift,gauss.key.s4,gauss.key.s4.e,gauss.key.s5,gauss.key.s5.hz,gauss.main,gauss.main.s1,gauss.main.s1.s1,gauss.main.s1.s2,gauss.main.s2,gauss.main.s2.s1,gauss.main.s2.s2,gauss.main.s2.s2.s1,gauss.main.s2.s2.s2· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:hodd,hodd.hint,hodd.hint.hjk,hodd.hint.s2,hodd.hint.s3,hodd.hint.s3.hP1,hodd.hint.s3.hP2,hodd.hint.s3.hP2.this,hodd.hint.s3.hP3,hodd.hint.s3.hcast,hodd.hint.s3.hdn,hodd.hint.s3.hdvd,hodd.hint.s3.hdvd.this,hodd.hint.s3.hmem,hodd.hint.s3.hne,hodd.hint.s3.hne.this,hodd.hint.s3.ht,hodd.hint.s3.s1,hodd.hint.s3.s9· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:combine,combine.hcop,combine.hdvd,combine.hint,combine.hint.this,combine.s2,combine.s5· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:hcore,hcore.hQcint,hcore.hQcint.s1,hcore.hQcint.s2,hcore.h_x3a9div,hcore.h_x3a9odd,hcore.h_x3a9odd.s1,hcore.h_x3a9odd.s2,hcore.h_x3a9odd.s3,hcore.h_x3a9odd.s3.ht1,hcore.h_x3a9odd.s3.ht1.this· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:hcore.hI,hcore.hI.h1,hcore.hI.h2,hcore.hK,hcore.hK.this,hcore.key1,hcore.key1.s1,hcore.key1.s1.h2a,hcore.key1.s1.hne,hcore.key1.s1.hne.this,hcore.key1.s1.s1,hcore.key1.s1.s2,hcore.key1.s1.this,hcore.key1.s2,hcore.key1.s2.h2b,hcore.key1.s2.hne,hcore.key1.s2.hne.this,hcore.key1.s2.s1,hcore.key1.s2.s2,hcore.key1.s2.this· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:hcore.h2adic,hcore.h2adic.htail,hcore.hB',hcore.hT,hcore.hT.hj',hcore.hT.hmono,hcore.hT.hne,hcore.hT.hne',hcore.hT.hne.this,hcore.hT.s2,hcore.hT.s3,hcore.hT.s5,hcore.s9· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:hcnall,hcnall.hint,hcnall.hint.s1,hcnall.hint.s1.hj',hcnall.hint.s1.s2,hcnall.hint.s1.s2.e,hcnall.hint.s1.s3,hcnall.hint.s1.s3.e,hcnall.hint.s2,hcnall.hint.s2.hmem,hcnall.hint.s2.hne,hcnall.hint.s2.hne.h8,hcnall.hint.s2.hne.h8.s1,hcnall.hint.s2.hne.h8.s2· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:hb,hb.key,hb.key.s1,hb.key.s2,hb.key.s2.hP1,hb.key.s2.hP2,hb.key.s2.hS1,hb.key.s2.hS1.e,hb.key.s2.hS2,hb.key.s2.hS2.this,hb.key.s2.hT,hb.key.s2.s3,hb.key.s2.s4· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:hb.key.s2.hexp,hb.key.s2.hexp.arith,hb.key.s2.hexp.arith.hsq,hb.key.s2.hexp.arith.s2,hb.key.s2.hexp.arith.s3,hb.key.s2.hexp.hT',hb.key.s2.hexp.hc',hb.key.s2.hexp.hd',hb.key.s2.hexp.s2,hb.key.s2.hexp.s3,hb.key.s2.hexp.this,hb.key.s2.s10,hb.key.s2.s11,hb.key.s2.s9· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:hqx,hqx.hterm,hqx.hterm.h2,hqx.hterm.hexp,hqx.hterm.hexp.e1,hqx.hterm.hexp.e2,hqx.hterm.hexp.e3,hqx.hterm.hexp.s4,hqx.hterm.hexp.s5,hqx.hterm.hkn,hqx.hterm.hpow,hqx.hterm.s2,hqx.hterm.s3,hqx.hterm.s4· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:hE,hE.s1,hE.s2,hE.s3,hE.s3.s1,hE.s3.s1.hm1,hE.s3.s1.hm1.this,hE.s3.s1.this,hE.s3.s1.this.s1,hE.s3.s1.this.s2,hE.s3.s2,hE.s3.s2.hj2,hE.s3.s2.this,hE.s3.s2.this.s1,hE.s3.s2.this.s2· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:hAqint,hAqint.s1,hAqint.s2,hAqint.s2.s1,hAqint.s2.s2,hAqint.s2.s2.hC,hAqint.s2.s2.hC.h3,hAqint.s2.s2.hC.h3.s1,hAqint.s2.s2.hC.h3.s2,hAqint.s2.s2.hC.hj2,hAqint.s2.s2.hM,hAqint.s2.s2.hQxn,hAqint.s2.s2.hd,hAqint.s2.s2.s4,hAqint.s2.s2.s5· Draft - erdos-1050--h1-v2--h3 · explainer of the proof ·
steps:hAqint.s2.s2.hterm,hAqint.s2.s2.hterm.e1,hAqint.s2.s2.hterm.h2n,hAqint.s2.s2.hterm.hexp,hAqint.s2.s2.hterm.hexp.e1,hAqint.s2.s2.hterm.hexp.e2,hAqint.s2.s2.hterm.hexp.e3,hAqint.s2.s2.hterm.hexp.s4,hAqint.s2.s2.hterm.hexp.s5,hAqint.s2.s2.hterm.hkn,hAqint.s2.s2.hterm.hpow,hAqint.s2.s2.hterm.s2,hAqint.s2.s2.hterm.s3,s21· Draft - erdos-1050--h1-v2--h4 · gloss of the statement ·
whole· Draft - erdos-1050--h1-v2--h4 · gloss of the witness ·
whole· Draft - erdos-1050--h1-v2--h4 · explainer of the proof ·
overview· Draft - erdos-1050--h1-v2--h4 · explainer of the proof ·
steps:id1_full,id1_test,lower_test,rhs_test,upper_test· Draft - erdos-1050--h1-v2--h4 · explainer of the proof ·
steps:lagr_eval,tail_coeff· Draft - erdos-1050--h1-v2--h4 · explainer of the proof ·
steps:split3T,tail3· Draft - erdos-1050--h1-v2--h4 · explainer of the proof ·
steps:cauchy_fin,h4_series· Draft - erdos-1050--h1-v2--h4 · explainer of the proof ·
steps:nd_bound,prod_one_sub_ge· Draft - erdos-1050--h1-v2--h4 · explainer of the proof ·
steps:h4_big,ineq_pow· Draft - erdos-1050--h1-v2--h4 · explainer of the proof ·
steps:T_facts,e,hAq0,hAq1,hQx0,hQx1,s17· Draft - spec-180d8b72 · gloss of the statement ·
whole· Draft - spec-180d8b72 · gloss of the witness ·
whole· Draft - spec-180d8b72 · explainer of the proof ·
overview· Draft - spec-180d8b72 · explainer of the proof ·
steps:id1_full,id1_test,lower_test,rhs_test,upper_test· Draft - spec-180d8b72 · explainer of the proof ·
steps:lagr_eval,tail_coeff· Draft - spec-180d8b72 · explainer of the proof ·
steps:split3T,tail3· Draft - spec-180d8b72 · explainer of the proof ·
steps:cauchy_fin,h4_series· Draft - spec-180d8b72 · explainer of the proof ·
steps:nd_bound,prod_one_sub_ge· Draft - spec-180d8b72 · explainer of the proof ·
steps:h4_big,ineq_pow· Draft - spec-180d8b72 · explainer of the proof ·
steps:T_facts,e,hAq0,hAq1,hQx0,hQx1,s17· Draft - spec-1a5ab7c3 · gloss of the statement ·
whole· Draft - spec-1a5ab7c3 · gloss of the witness ·
whole· Draft - spec-1a5ab7c3 · explainer of the proof ·
overview· Draft - spec-1a5ab7c3 · explainer of the proof ·
steps:key,key.h1,key.h1.this,key.hle,key.hlt,key.hlt.this,key.hmem,key.hmem.s1,key.hmem.s1.this,key.hmem.s2,key.ht1· Draft - spec-1a5ab7c3 · explainer of the proof ·
steps:s2· Draft - spec-1a5ab7c3 · explainer of the proof ·
steps:s3,s3.hP,s3.hP.this,s3.hne,s3.hneq,s3.s1· Draft - spec-440db0f9 · gloss of the statement ·
whole· Draft - spec-440db0f9 · gloss of the witness ·
whole· Draft - spec-440db0f9 · explainer of the proof ·
overview· Draft - spec-440db0f9 · explainer of the proof ·
steps:hD,hD.h1,hDk· Draft - spec-440db0f9 · explainer of the proof ·
steps:key,key.hDj,key.hj,key.hshift,key.s4,key.s4.e,key.s5,key.s5.hz· Draft - spec-440db0f9 · explainer of the proof ·
steps:main,main.s1,main.s1.s1,main.s1.s2,main.s2,main.s2.s1,main.s2.s2,main.s2.s2.s1,main.s2.s2.s2· Draft - spec-eb1219eb · gloss of the statement ·
whole· Draft - spec-eb1219eb · gloss of the witness ·
whole· Draft - spec-eb1219eb · explainer of the proof ·
overview· Draft - spec-eb1219eb · explainer of the proof ·
steps:s1,s1.s1,s1.s2· Draft - spec-eb1219eb · explainer of the proof ·
steps:s2,s2.s1,s2.s2· Draft - spec-f2b55478 · gloss of the statement ·
whole· Draft - spec-f2b55478 · gloss of the witness ·
whole· Draft - spec-f2b55478 · explainer of the proof ·
overview· Draft - spec-f2b55478 · explainer of the proof ·
steps:hres,hres.E1test,hres.E1test.s1,hres.E1test.s2,hres.E2test,hres.E3test,hres.E4test,hres.F1,hres.F2,hres.F3,hres.hA,hres.hA.this,hres.hAj,hres.hQ,hres.hQ.this,hres.hQj,hres.hQr,hres.hp,hres.hp.h2,hres.hp.s2,hres.hp.s3,hres.s1· Draft - spec-f2b55478 · explainer of the proof ·
steps:hpf,hpf.hE1,hpf.hE1.hk',hpf.hE1.this,hpf.hE2,hpf.hdeg,hpf.hev,hpf.hinj,hpf.hj',hpf.hxj,hpf.hxj.this,hpf.key· Draft - spec-f2b55478 · explainer of the proof ·
steps:hl,hl.h2,hl.hj',hl.hp· Draft - spec-f2b55478 · explainer of the proof ·
steps:hr,hr.hB,hr.hB.this,hr.key,hr.s3,hr.s3.hA,hr.s3.hA.e,hr.s3.hD,hr.s3.hD.e,hr.s3.hDX,hr.s3.hDX.this,hr.s3.hs,hr.s4,hr.s4.hz1,hr.s4.hz2· Draft - spec-ffd3137a · gloss of the statement ·
whole· Draft - spec-ffd3137a · gloss of the witness ·
whole· Draft - spec-ffd3137a · explainer of the proof ·
overview· Draft - spec-ffd3137a · explainer of the proof ·
steps:lag_test,lag_test.hB,lag_test.hF,lag_test.hb,lag_test.hb.h1,lag_test.hb.h1.hl',lag_test.hb.h1.this,lag_test.hb.hs',lag_test.hc,lag_test.hc.s1,lag_test.hc.s2,lag_test.hd,lag_test.hd.s1,lag_test.hd.s2,lag_test.he,lag_test.he.hn,lag_test.he.ht',lag_test.hf,lag_test.hf.hi',lag_test.hjj,lag_test.hjj.h2,lag_test.hjj.s2,lag_test.hjj.s3,lag_test.hpos,lag_test.hpos.this,lag_test.hpos.this.s1,lag_test.hpos.this.s2,lag_test.hpow· Draft - spec-ffd3137a · explainer of the proof ·
steps:pf_test,pf_test.hE,pf_test.hL,pf_test.s3,pf_test.s3.s1,pf_test.s3.s2,pf_test.s4,pf_test.s4.s1,pf_test.s4.s2,pf_test.s4.s3,pf_test.s4.s4· Draft - spec-ffd3137a · explainer of the proof ·
steps:pf2_test,pf2_test.h1,pf2_test.h1',pf2_test.h1.hjk,pf2_test.h1.hjs,pf2_test.h1.hks,pf2_test.h1.s4,pf2_test.h1.s4.this,pf2_test.h1.s5,pf2_test.h1.s6,pf2_test.h2,pf2_test.h2.this,pf2_test.h3,pf2_test.h3.this,pf2_test.hLE,pf2_test.hP0,pf2_test.hd,pf2_test.hne· Draft - spec-ffd3137a · explainer of the proof ·
steps:h2,hc,hinj,hinj.this,hk1,hpf,hpk,hs1,hs1',hs1.this,hs1.this.s1,hs1.this.s2,hw,hw.e1,hw.e2,hw.e3,hw.e3.ga,hw.e3.ga.this,hw.e3.gb,hw.hjn,hx,hxy,hxy.this· Draft - spec-ffd3137a · explainer of the proof ·
steps:T0,T1,T1.e1,T1.ga,T1.ga.hjk,T1.gb,T1.gb.this,T2,T2.e,T2.this,T3,T3a,T3a.e1,T3a.ha,T3a.ha.this,T3a.hb,T3b,T3b.e1,T3b.e1.hlk,T3b.this,T3c,T3c.this· Draft
- erdos-1094 · gloss of the statement ·
whole· Draft - erdos-1094 · gloss of the witness ·
whole· Draft - erdos-1094 · explainer of the partial ·
overview· Draft - erdos-1094 · explainer of the partial ·
steps:hall· Draft - erdos-1094 · explainer of the partial ·
steps:s2· Draft - erdos-1094 · explainer of the partial ·
steps:hT· Draft - erdos-1094 · explainer of the partial ·
steps:s4· Draft - erdos-1094 · explainer of the partial ·
steps:s5· Draft - erdos-1094 · gloss of the partial ·
whole· Draft - erdos-1094--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h1 · explainer of the proof ·
overview· Draft - erdos-1094--h1 · explainer of the proof ·
steps:s1· Draft - erdos-1094--h1 · explainer of the proof ·
steps:hkt,hm_gt,hm_le,htpos· Draft - erdos-1094--h1 · explainer of the proof ·
steps:hnd· Draft - erdos-1094--h1 · explainer of the proof ·
steps:hcop· Draft - erdos-1094--h1 · explainer of the proof ·
steps:hm_dvd· Draft - erdos-1094--h1 · explainer of the proof ·
steps:close,hle,hm_fact· Draft - erdos-1094--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h2 · gloss of the partial ·
whole· Draft - erdos-1094--h2--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h1 · explainer of the partial ·
overview· Draft - erdos-1094--h2--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h1--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h1--h1--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h1--h1--h1--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h1--h1--h1--h1--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h1--h1--h1--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h1--h1--h1--h2--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h1--h1--h1--h2--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h1--h4 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h1--h4--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h1--h4--h1 · gloss of the partial ·
whole· Draft - erdos-1094--h2--h1--h4--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h1--h4--h1--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h1--h4--h1--h2--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h2--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h2--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h2--h2 · gloss of the partial ·
whole· Draft - erdos-1094--h2--h2--h2--h2--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h2--h3 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h2--h3 · gloss of the partial ·
whole· Draft - erdos-1094--h2--h2--h2--h3--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h2--h3--h1 · gloss of the partial ·
whole· Draft - erdos-1094--h2--h2--h2--h3--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h2--h3--h1--h1 · gloss of the partial ·
whole· Draft - erdos-1094--h2--h2--h2--h3--h1--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h2--h3--h1--h1--h1 · gloss of the partial ·
whole· Draft - erdos-1094--h2--h2--h2--h3--h1--h1--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h2--h4 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h2--h4 · gloss of the partial ·
whole· Draft - erdos-1094--h2--h2--h3 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h3--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h2--h2--h3--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3 · gloss of the statement ·
whole· Draft - erdos-1094--h3 · explainer of the partial ·
overview· Draft - erdos-1094--h3 · explainer of the partial ·
steps:h_sieve· Draft - erdos-1094--h3 · explainer of the partial ·
steps:s2· Draft - erdos-1094--h3 · explainer of the partial ·
steps:hKk· Draft - erdos-1094--h3 · explainer of the partial ·
steps:s4· Draft - erdos-1094--h3 · explainer of the partial ·
steps:hdvd,hfact,hmodeq,hzero· Draft - erdos-1094--h3 · explainer of the partial ·
steps:close,hle· Draft - erdos-1094--h3 · gloss of the partial ·
whole· Draft - erdos-1094--h3--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1 · gloss of the partial ·
whole· Draft - erdos-1094--h3--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h1 · gloss of the partial ·
whole· Draft - erdos-1094--h3--h1--h1 · gloss of the partial ·
whole· Draft - erdos-1094--h3--h1--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h1--h1 · gloss of the partial ·
whole· Draft - erdos-1094--h3--h1--h1--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h1--h1--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h1--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h1--h2 · gloss of the partial ·
whole· Draft - erdos-1094--h3--h1--h1--h2--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h1--h2--h1 · gloss of the partial ·
whole· Draft - erdos-1094--h3--h1--h1--h2--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h1--h2--h1--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h1--h3 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h2 · gloss of the partial ·
whole· Draft - erdos-1094--h3--h1--h2--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h2--h1 · gloss of the partial ·
whole· Draft - erdos-1094--h3--h1--h2--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h2--h1--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h2--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h2--h2 · gloss of the partial ·
whole· Draft - erdos-1094--h3--h1--h2--h2--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h2--h2--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h2--h2--h2--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h1--h2--h2--h2--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h2--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h2--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h2--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h2--h3 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h3 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h3--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h3--h1 · gloss of the partial ·
whole· Draft - erdos-1094--h3--h3--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h3--h1--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h3--h1--h1--h1--h1 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h3--h1--h1--h1--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h3--h2 · gloss of the statement ·
whole· Draft - erdos-1094--h3--h3--h2 · gloss of the partial ·
whole· Draft - erdos-1094--h3--h3--h2--h1 · gloss of the statement ·
whole· Draft
- erdos-1094--h2 · Open problem: no proof is known · proposed by
t1009-b· 2026-10-09T12:51:37Z · record - erdos-1094--h2--h1 · Known: a proof is published and not formalised · proposed by
t1009-b· 2026-10-09T13:09:04Z · record - erdos-1094--h2--h1--h1 · Known: a proof is published and not formalised · proposed by
t1009-c· 2026-10-09T14:48:17Z · record - erdos-1094--h2--h1--h4 · Known: a proof is published and not formalised · proposed by
t1014-z· 2026-10-14T11:20:02Z · record - erdos-1094--h2--h2--h1 · Known: a proof is published and not formalised · proposed by
t1014-z· 2026-10-14T11:19:14Z · record - erdos-1094--h2--h2--h2 · Known: a proof is published and not formalised · proposed by
t1014-x· 2026-10-14T11:24:47Z · record - erdos-1094--h3 · Known: a proof is published and not formalised · proposed by
t1009-a· 2026-10-09T12:57:00Z · record - erdos-1094--h3--h2--h1 · Known: a proof is published and not formalised · proposed by
t1016-lit· 2026-10-16T12:14:34Z · record - erdos-1094--h3--h2--h2 · Known: a proof is published and not formalised · proposed by
t1016-lit· 2026-10-16T12:14:38Z · record - erdos-1094--h3--h2--h3 · Known: a proof is published and not formalised · proposed by
t1016-lit· 2026-10-16T12:15:03Z · record - erdos-1094--h3--h3--h1--h1 · Known: a proof is published and not formalised · proposed by
t1016-lit· 2026-10-16T12:14:25Z · record - erdos-1094--h3--h3--h2--h1 · Known: a proof is published and not formalised · proposed by
t1016-lit· 2026-10-16T12:14:30Z · record
- erdos-257 · gloss of the statement ·
whole· Draft - erdos-257 · explainer of the partial ·
overview· Draft - erdos-257 · explainer of the partial ·
steps:h_core,h_greedy· Draft - erdos-257 · explainer of the partial ·
steps:h0,hA'· Draft - erdos-257 · explainer of the partial ·
steps:close,hgr,hsum· Draft - erdos-257--h1 · gloss of the statement ·
whole· Draft - erdos-257--h1 · explainer of the proof ·
overview· Draft - erdos-257--h1 · explainer of the proof ·
steps:e1,e2,hf· Draft - erdos-257--h1 · explainer of the proof ·
steps:e3,e4,htail_nonneg· Draft - erdos-257--h1 · explainer of the proof ·
steps:s7· Draft - erdos-257--h1 · explainer of the proof ·
steps:s8· Draft - erdos-257--h18 · gloss of the statement ·
whole· Draft - erdos-257--h2 · gloss of the statement ·
whole· Draft - erdos-257--h2 · explainer of the partial ·
overview· Draft - erdos-257--h2 · explainer of the partial ·
steps:h_walk· Draft - erdos-257--h2 · explainer of the partial ·
steps:s2· Draft - erdos-257--h2 · explainer of the partial ·
steps:s3· Draft - erdos-257--h2--h1 · gloss of the statement ·
whole· Draft - spec-137537c8 · gloss of the statement ·
whole· Draft - spec-137537c8 · explainer of the proof ·
overview· Draft - spec-137537c8 · explainer of the proof ·
steps:h0B,he_summable,hg_nonneg,hg_summable,hrow,hrow_summable· Draft - spec-137537c8 · explainer of the proof ·
steps:hL,hmid· Draft - spec-137537c8 · explainer of the proof ·
steps:hR,hfib· Draft - spec-23b0fff0 · gloss of the statement ·
whole· Draft - spec-23b0fff0 · explainer of the proof ·
overview· Draft - spec-23b0fff0 · explainer of the proof ·
steps:hF_le,hFs,hlam· Draft - spec-23b0fff0 · explainer of the proof ·
steps:hjeq· Draft - spec-23b0fff0 · explainer of the proof ·
steps:hb,hshift,hsplit· Draft - spec-23b0fff0 · explainer of the proof ·
steps:h2j,hT,hb',s11,s12· Draft - spec-5e2e0890 · gloss of the statement ·
whole· Draft - spec-5e2e0890 · explainer of the proof ·
overview· Draft - spec-5e2e0890 · explainer of the proof ·
steps:h1,h3· Draft - spec-5e2e0890 · explainer of the proof ·
steps:hex,hmin,hn· Draft - spec-5e2e0890 · explainer of the proof ·
steps:hnonneg· Draft - spec-5e2e0890 · explainer of the proof ·
steps:s7· Draft - spec-5e2e0890 · explainer of the proof ·
steps:s8· Draft - spec-5e2e0890 · explainer of the partial ·
overview· Draft - spec-5e2e0890 · explainer of the partial ·
steps:h1,h3· Draft - spec-5e2e0890 · explainer of the partial ·
steps:hex,hmin,hn· Draft - spec-5e2e0890 · explainer of the partial ·
steps:hnonneg· Draft - spec-5e2e0890 · explainer of the partial ·
steps:s7,s8· Draft - spec-5e2e0890--h1 · gloss of the statement ·
whole· Draft - spec-5e2e0890--h1 · explainer of the proof ·
overview· Draft - spec-5e2e0890--h1 · explainer of the proof ·
steps:hgeom· Draft - spec-5e2e0890--h1 · explainer of the proof ·
steps:s2· Draft - spec-5e2e0890--h1 · explainer of the proof ·
steps:s3· Draft - spec-5e2e0890--h2 · gloss of the statement ·
whole· Draft - spec-5e2e0890--h2 · explainer of the proof ·
overview· Draft - spec-5e2e0890--h2 · explainer of the proof ·
steps:hL,hS_sup,hT_sub,hdisj1,hdisj2,hmono,hsum,htail· Draft - spec-5e2e0890--h2 · explainer of the proof ·
steps:s10,s11,s12,s13,s14,s15,s9· Draft - spec-689ac1ac · gloss of the statement ·
whole· Draft - spec-689ac1ac · explainer of the proof ·
overview· Draft - spec-689ac1ac · explainer of the proof ·
steps:hF_le,hFeq,hFeqN,hFs· Draft - spec-689ac1ac · explainer of the proof ·
steps:hTsum,hTy,hTyk,hZ· Draft - spec-689ac1ac · explainer of the proof ·
steps:hsplit· Draft - spec-689ac1ac · explainer of the proof ·
steps:hdiv· Draft - spec-689ac1ac · explainer of the proof ·
steps:h2k,hi',key· Draft - spec-a70fcca4 · explainer of the partial ·
overview· Draft - spec-a70fcca4 · explainer of the partial ·
steps:h1,h2,h3,h4· Draft - spec-a70fcca4 · explainer of the partial ·
steps:hex,s6· Draft - spec-a70fcca4 · explainer of the partial ·
steps:hr,htail· Draft - spec-a70fcca4 · explainer of the partial ·
steps:hfnn,hpart,hsum· Draft - spec-a70fcca4 · explainer of the partial ·
steps:s12· Draft - spec-a70fcca4 · explainer of the partial ·
steps:s13· Draft - spec-a70fcca4--h1 · gloss of the statement ·
whole· Draft - spec-a70fcca4--h1 · gloss of the witness ·
whole· Draft - spec-a70fcca4--h1 · explainer of the proof ·
overview· Draft - spec-a70fcca4--h1 · explainer of the proof ·
steps:s1· Draft - spec-a70fcca4--h1 · explainer of the proof ·
steps:s2· Draft - spec-a70fcca4--h2 · gloss of the statement ·
whole· Draft - spec-a70fcca4--h2 · gloss of the witness ·
whole· Draft - spec-a70fcca4--h2 · explainer of the proof ·
overview· Draft - spec-a70fcca4--h2 · explainer of the proof ·
steps:key· Draft - spec-a70fcca4--h2 · explainer of the proof ·
steps:close,h2,h3,hqne,s2· Draft - spec-a70fcca4--h3 · gloss of the statement ·
whole· Draft - spec-a70fcca4--h3 · gloss of the witness ·
whole· Draft - spec-a70fcca4--h3 · explainer of the proof ·
overview· Draft - spec-a70fcca4--h3 · explainer of the proof ·
steps:hnn· Draft - spec-a70fcca4--h3 · explainer of the proof ·
steps:hle· Draft - spec-a70fcca4--h3 · explainer of the proof ·
steps:close· Draft - spec-a70fcca4--h4 · gloss of the statement ·
whole· Draft - spec-a70fcca4--h4 · gloss of the witness ·
whole· Draft - spec-a70fcca4--h4 · explainer of the partial ·
overview· Draft - spec-a70fcca4--h4 · explainer of the partial ·
overview· Draft - spec-a70fcca4--h4--h1 · gloss of the statement ·
whole· Draft - spec-a70fcca4--h4--h1 · gloss of the witness ·
whole· Draft - spec-a70fcca4--h4--h1 · explainer of the partial ·
steps:hrun· Draft - spec-a70fcca4--h4--h1 · explainer of the partial ·
steps:hup· Draft - spec-a70fcca4--h4--h1 · explainer of the partial ·
steps:hblock· Draft - spec-a70fcca4--h4--h1 · explainer of the partial ·
steps:s4· Draft - spec-a70fcca4--h4--h1 · explainer of the partial ·
steps:s5· Draft - spec-a70fcca4--h4--h1 · explainer of the partial ·
overview· Draft - spec-a70fcca4--h4--h1--h1 · gloss of the statement ·
whole· Draft - spec-a70fcca4--h4--h1--h1 · gloss of the witness ·
whole· Draft - spec-a70fcca4--h4--h1--h2 · gloss of the statement ·
whole· Draft - spec-a70fcca4--h4--h1--h2 · gloss of the witness ·
whole· Draft - spec-a70fcca4--h4--h1--h2 · explainer of the partial ·
overview· Draft - spec-a70fcca4--h4--h1--h2--h1 · gloss of the statement ·
whole· Draft - spec-a70fcca4--h4--h2 · gloss of the statement ·
whole· Draft - spec-a70fcca4-v2 · gloss of the statement ·
whole· Draft - spec-a70fcca4-v2 · gloss of the witness ·
whole· Draft - spec-a70fcca4-v2 · gloss of the relation ·
whole· Draft - spec-ced1e7c5 · gloss of the statement ·
whole· Draft - spec-ddd99827 · gloss of the statement ·
whole· Draft - spec-ddd99827 · explainer of the proof ·
overview· Draft - spec-ddd99827 · explainer of the proof ·
steps:h2n,hpos1· Draft - spec-ddd99827 · explainer of the proof ·
steps:hnonneg,hterm· Draft - spec-ddd99827 · explainer of the proof ·
steps:hgeom,hle,hsum· Draft - spec-ddd99827 · explainer of the proof ·
steps:s8,s9· Draft - variant-037e597d · gloss of the statement ·
whole· Draft - variant-1629563f · gloss of the statement ·
whole· Draft - variant-2a349f4f · gloss of the statement ·
whole· Draft - variant-2a349f4f · explainer of the proof ·
overview· Draft - variant-2a349f4f · explainer of the proof ·
steps:close· Draft - variant-2f5236aa · gloss of the statement ·
whole· Draft - variant-2f5236aa · gloss of the relation ·
whole· Draft - variant-2f5236aa · explainer of the proof ·
overview· Draft - variant-2f5236aa · explainer of the proof ·
steps:close· Draft - variant-41d1f19b · gloss of the statement ·
whole· Draft - variant-5274cf38 · gloss of the statement ·
whole· Draft - variant-5274cf38 · gloss of the relation ·
whole· Draft - variant-5274cf38 · explainer of the proof ·
overview· Draft - variant-5274cf38--h1 · gloss of the statement ·
whole· Draft - variant-5274cf38--h1--h1 · gloss of the statement ·
whole· Draft - variant-5c939e77 · gloss of the statement ·
whole· Draft - variant-6b364d2b · gloss of the statement ·
whole· Draft - variant-6b364d2b · gloss of the relation ·
whole· Draft - variant-6b364d2b--h1 · gloss of the statement ·
whole· Draft - variant-6b364d2b--h1--h1 · gloss of the statement ·
whole· Draft - variant-77c0756e · gloss of the statement ·
whole· Draft - variant-7a0f5735 · gloss of the statement ·
whole· Draft - variant-7a0f5735 · gloss of the relation ·
whole· Draft - variant-7a0f5735 · explainer of the proof ·
overview· Draft - variant-7a0f5735 · explainer of the proof ·
steps:close· Draft - variant-886b66da · gloss of the statement ·
whole· Draft - variant-886b66da · gloss of the relation ·
whole· Draft - variant-886b66da · explainer of the proof ·
overview· Draft - variant-90827f46 · gloss of the statement ·
whole· Draft - variant-970a2ffa · gloss of the statement ·
whole· Draft - variant-970a2ffa · gloss of the relation ·
whole· Draft - variant-970a2ffa · explainer of the proof ·
overview· Draft - variant-970a2ffa · explainer of the proof ·
steps:close· Draft - variant-c91009b9 · gloss of the statement ·
whole· Draft - variant-c91009b9 · gloss of the relation ·
whole· Draft - variant-c91009b9 · explainer of the proof ·
overview· Draft - variant-d08712d9 · gloss of the statement ·
whole· Draft - variant-d144ccc1 · gloss of the statement ·
whole· Draft - variant-f93b89d8 · gloss of the statement ·
whole· Draft - variant-f9c7b81b · gloss of the statement ·
whole· Draft - variant-f9c7b81b · explainer of the proof ·
overview· Draft
- erdos-257 · Open problem: no proof is known · proposed by
t1022-d· 2026-10-22T12:39:00Z · record - erdos-257--h2 · Open problem: no proof is known · proposed by
t1022-d· 2026-10-22T16:02:15Z · record - spec-5e2e0890 · Elementary: a routine formalisation of a known fact · proposed by
t1022-d· 2026-10-22T13:00:23Z · record - spec-a70fcca4--h4 · Open problem: no proof is known · proposed by
t1022-d· 2026-10-22T16:04:00Z · record - spec-a70fcca4-v2 · Open problem: no proof is known · proposed by
t1022-d· 2026-10-22T15:56:45Z · record - spec-ddd99827 · Elementary: a routine formalisation of a known fact · proposed by
t1022-d· 2026-10-23T04:23:45Z · record - variant-2f5236aa · Known: a proof is published and not formalised · proposed by
t1022-d· 2026-10-22T12:57:49Z · record - variant-5274cf38 · Known: a proof is published and not formalised · proposed by
t1022-d· 2026-10-22T13:56:24Z · record - variant-5274cf38--h1 · Known: a proof is published and not formalised · proposed by
t1026-b· 2026-10-26T21:04:07Z · record - variant-5274cf38--h1--h1 · Known: a proof is published and not formalised · proposed by
t1026-b· 2026-10-26T21:35:36Z · record - variant-5c939e77 · Elementary: a routine formalisation of a known fact · proposed by
t1022-d· 2026-10-22T15:22:15Z · record - variant-6b364d2b · Known: a proof is published and not formalised · proposed by
t1022-d· 2026-10-22T13:47:27Z · record - variant-7a0f5735 · Known: a proof is published and not formalised · proposed by
t1022-d· 2026-10-22T15:29:44Z · record - variant-886b66da · Known: a proof is published and not formalised · proposed by
t1022-d· 2026-10-22T13:56:19Z · record - variant-970a2ffa · Known: a proof is published and not formalised · proposed by
t1022-d· 2026-10-22T14:49:18Z · record - variant-c91009b9 · Known: a proof is published and not formalised · proposed by
t1022-d· 2026-10-22T14:13:17Z · record - variant-d08712d9 · Known: a proof is published and not formalised · proposed by
t1022-d· 2026-10-23T04:23:37Z · record - variant-f9c7b81b · Elementary: a routine formalisation of a known fact · proposed by
t1022-d· 2026-10-22T13:43:15Z · record
- erdos-402--h1 · gloss of the statement ·
whole· Draft - erdos-402--h2 · gloss of the statement ·
whole· Draft - erdos-402--h2-v2 · gloss of the statement ·
whole· Draft - erdos-402--h3 · gloss of the statement ·
whole· Draft - erdos-402--h3-v2 · gloss of the statement ·
whole· Draft - erdos-402--h3-v2--h1 · gloss of the statement ·
whole· Draft - erdos-402--h3-v2--h1--h1 · gloss of the statement ·
whole· Draft - erdos-402--h3-v2--h1--h1--h1 · gloss of the statement ·
whole· Draft - erdos-402--h3-v2--h1--h1--h1--h1 · gloss of the statement ·
whole· Draft - erdos-402--h3-v2--h1--h1--h1--h2 · gloss of the statement ·
whole· Draft - erdos-402--h3-v2--h1--h1--h1--h2--h1 · gloss of the statement ·
whole· Draft - erdos-402--h3-v2--h1--h1--h1--h2--h2 · gloss of the statement ·
whole· Draft - erdos-402--h3-v2--h1--h1--h1--h2--h3 · gloss of the statement ·
whole· Draft - spec-48bd0126 · gloss of the statement ·
whole· Draft - spec-fa8046e4 · gloss of the statement ·
whole· Draft - variant-11152e83 · gloss of the statement ·
whole· Draft - variant-29101bbc · gloss of the statement ·
whole· Draft - variant-3377fd96 · gloss of the statement ·
whole· Draft - variant-4ad214d0 · gloss of the statement ·
whole· Draft - variant-64035064 · gloss of the statement ·
whole· Draft - variant-6bb50ad7 · gloss of the statement ·
whole· Draft - variant-6bd06d63 · gloss of the statement ·
whole· Draft - variant-77918742 · gloss of the statement ·
whole· Draft - variant-780e7ade · gloss of the statement ·
whole· Draft - variant-7a4bb0cd · gloss of the statement ·
whole· Draft - variant-892f5809 · gloss of the statement ·
whole· Draft - variant-950630b9 · gloss of the statement ·
whole· Draft - variant-9724698e · gloss of the statement ·
whole· Draft - variant-a3b3cb8f · gloss of the statement ·
whole· Draft - variant-a5969ff3 · gloss of the statement ·
whole· Draft - variant-a874fe93 · gloss of the statement ·
whole· Draft - variant-b89de5c4 · gloss of the statement ·
whole· Draft - variant-bc28297c · gloss of the statement ·
whole· Draft - variant-d865c9c6 · gloss of the statement ·
whole· Draft - variant-e6d83e6d · gloss of the statement ·
whole· Draft
- erdos-412--h1 · gloss of the statement ·
whole· Draft - erdos-412--h1-v2 · gloss of the statement ·
whole· Draft
- erdos-69--h1 · gloss of the statement ·
whole· Draft - erdos-69--h1-v2 · gloss of the statement ·
whole· Draft - erdos-69--h2 · gloss of the statement ·
whole· Draft - erdos-69--h2-v2 · gloss of the statement ·
whole· Draft - erdos-69--h2-v2 · gloss of the partial ·
whole· Draft - erdos-69--h2-v2--h1 · gloss of the statement ·
whole· Draft - erdos-69--h2-v2--h1-v2 · gloss of the statement ·
whole· Draft - erdos-69--h2-v2--h1-v2 · gloss of the partial ·
whole· Draft - erdos-69--h2-v2--h1-v2--h1 · gloss of the statement ·
whole· Draft - erdos-69--h2-v2--h1-v2--h2 · gloss of the statement ·
whole· Draft - erdos-69--h2-v2--h1-v2--h3 · gloss of the statement ·
whole· Draft - erdos-69--h2-v2--h1-v2--h4 · gloss of the statement ·
whole· Draft - spec-13f68833 · gloss of the statement ·
whole· Draft - spec-2e765953 · gloss of the statement ·
whole· Draft - spec-7d098d5c · gloss of the statement ·
whole· Draft - spec-7f0efe19 · gloss of the statement ·
whole· Draft - spec-84446025 · gloss of the statement ·
whole· Draft - spec-9f8cb4ea · gloss of the statement ·
whole· Draft - spec-c390279b · gloss of the statement ·
whole· Draft - spec-e0b917d1 · gloss of the statement ·
whole· Draft - variant-09e95e7a · gloss of the statement ·
whole· Draft - variant-09e95e7a · explainer of the proof ·
overview· Draft - variant-09e95e7a · explainer of the proof ·
steps:f_le,f_le.s1,f_le.s2,f_nonneg,hs· Draft - variant-09e95e7a · explainer of the proof ·
steps:comp,comp.hd,comp.hd.e,comp.hd.this,comp.s2,comp.s3,comp.s3.this,kpos· Draft - variant-09e95e7a · explainer of the proof ·
steps:hg,hg',hg'.this,split1,split2,split2',zero_part,zero_part.this· Draft - variant-09e95e7a · explainer of the proof ·
steps:Rpos,Rpos.hpi,Rpos.s1· Draft - variant-09e95e7a · explainer of the proof ·
steps:Rle,Rle.s1,Rle.s2,geo,geo.this,key,key.h1,key.s2,key.s3· Draft - variant-09e95e7a · explainer of the proof ·
steps:hZ',hZ'.hi',hZ'.s2,hZ'.s2.e,hZ'.s3· Draft - variant-09e95e7a · explainer of the proof ·
steps:hm,hqk,hx,i1,i2,mlt,mlt.h2,mlt.hk0,mlt.hk2,mlt.s4,mlt.s5,mlt.s6,mpos,mpos.this· Draft - variant-14c6c771 · gloss of the statement ·
whole· Draft - variant-3a1bcb9a · gloss of the statement ·
whole· Draft - variant-f592e3ab · gloss of the statement ·
whole· Draft
- erdos-849 · gloss of the statement ·
whole· Draft - erdos-849 · gloss of the witness ·
whole· Draft
- erdos-849 · Open problem: no proof is known · proposed by
t1026e-b· 2026-10-26T21:13:41Z · record - variant-293c7f51 · Elementary: a routine formalisation of a known fact · proposed by
t1026e-b· 2026-10-26T21:16:26Z · record - variant-c9253839 · Elementary: a routine formalisation of a known fact · proposed by
t1026e-b· 2026-10-26T21:16:20Z · record
- infinitude-of-primes · explainer of the proof ·
overview· Draft - infinitude-of-primes · explainer of the proof ·
steps:dvd_consecutive,dvd_fact,fact_pos,prime_divisor· Draft - infinitude-of-primes · explainer of the proof ·
steps:two_le,two_le.this· Draft - infinitude-of-primes · explainer of the proof ·
steps:s6· Draft - infinitude-of-primes · explainer of the proof ·
steps:s7,s8· Draft - infinitude-of-primes · explainer of the proof ·
steps:s8.h1,s8.h2,s8.hpos,s8.hpos.this,s8.this· Draft - infinitude-of-primes · gloss of the partial ·
whole· Draft - infinitude-of-primes--h2 · gloss of the statement ·
whole· Draft - infinitude-of-primes--h3 · gloss of the statement ·
whole· Draft - infinitude-of-primes--h3 · gloss of the witness ·
whole· Draft - infinitude-of-primes--h4 · gloss of the statement ·
whole· Draft - variant-2a7919a9 · gloss of the statement ·
whole· Draft - variant-2a7919a9 · gloss of the partial ·
whole· Draft - variant-2a7919a9--h1 · gloss of the statement ·
whole· Draft - variant-2a7919a9--h2 · gloss of the statement ·
whole· Draft - variant-4cb87a03 · gloss of the statement ·
whole· Draft - variant-6e71b160 · gloss of the statement ·
whole· Draft - variant-aceabdc4 · gloss of the statement ·
whole· Draft - variant-dea95969 · gloss of the statement ·
whole· Draft - variant-f15ce396 · gloss of the statement ·
whole· Draft - variant-f15ce396 · gloss of the relation ·
whole· Draft - IsPrime.lean · gloss of the definition ·
whole· Draft - infinitude-of-primes · gloss of the partial ·
whole· Draft
- variant-93e79cb5 · gloss of the statement ·
whole· Draft - variant-93e79cb5 · gloss of the partial ·
whole· Draft - variant-93e79cb5--h1 · gloss of the statement ·
whole· Draft - variant-93e79cb5--h2 · gloss of the statement ·
whole· Draft