A dataset of formal proofs in lean from the 1000 theorems project, for integration into the MaRDI knowledge graph.

The dataset was created by the following python code in the context of https://github.com/MaRDI4NFDI/MaRDIRoadmap/issues/65: import yamlimport pandas as pd#obtained from https://github.com/leanprover-community/mathlib4/blob/master/docs/1000.yamlwith open("~/1000.yaml",encoding='utf-8') as stream: theorems_dict = yaml.safe_load(stream)theorems_project_df = pd.DataFrame(theorems_dict).transpose()theorems_project_df.index.name = 'wikidata_qid'sparql_query = 'https://w.wiki/HcXE'#theorems from wikidata with english-language wikipedia article. obtained from wikidata via query https://w.wiki/HcXEnamed_theorems_json = '~/Downloads/named_theorems.json'with open(named_theorems_json, encoding='utf-8') as named_theorems_fh: named_theorems = json.load(named_theorems_fh)theorems_df = pd.read_json(named_theorems_json)theorems_df['wikidata_qid'] = theorems_df.cid.apply(lambda x:x.split('/')[-1])theorems_df = theorems_df.join(theorems_project_df,how='outer',on='wikidata_qid')theorems_df['P31'] = 'Q6480412'theorems_df['P37']='Q6480413'theorems_df['P1603']=theorems_df.apply(lambda x:x['decl'] if x['decl'] else x['url'],axis=1)theorems_df['P1460'] = 'Q6534201'theorems_df['P12'] = theorems_df['wikidata_qid']theorems_df = theorems_df.rename({'date':'P140','comment':'Den','title':'Len'})theorems_df['P205'] = theorems_df.apply(lambda x:"https://leanprover-community.github.io/1000.html#"+x['P12'] if x['decl'] or x['url'] else '')theorems_df['P1648'] = 'Q27041'formal_proofs_df = theorems_df.drop(columns=['P1460','P37','P31','P1603','cid','label','article','decl','authors','url','statement'])formal_proofs_df = formal_proofs_df.dropna(columns=['P205'])formal_proofs_df.fillna('').to_csv('~/formal_proofs_mardi.csv',index=False)