{"id":"W4302820658","doi":"10.3233/978-1-61499-419-0-93","title":"Formalization, Mechanization and Automation of G\\\"odel's Proof of God's Existence","year":2013,"lang":"en","type":"preprint","venue":"arXiv (Cornell University)","topic":"Classical Philosophy and Thought","field":"Arts and Humanities","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"","funders":"","keywords":"Proof assistant; Axiom; Programming language; Formality; Automated theorem proving; Computer science; Natural deduction; Consistency (knowledge bases); Structural proof theory; Proof theory; Automation; Mathematics; Calculus (dental); Discrete mathematics; Mathematical proof; Artificial intelligence; Linguistics; Philosophy; Engineering","routes":{"ca_aff":false,"ca_fund":false,"ca_venue":false,"about_ca":true,"invisible_to_affiliation_only":true},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002598705,0.0005887431,0.0005059309,0.001600382,0.00112103,0.002246279,0.001805645,0.0007223971,0.006966959],"category_scores_gemma":[0.00482362,0.0005359616,0.001610166,0.0005853544,0.005763486,0.002650909,0.004808016,0.002631737,0.001593356],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002105532,"about_ca_system_score_gemma":0.002325938,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003523728,"about_ca_topic_score_gemma":0.003596662,"domain_scores_codex":[0.9981528,0.0005467603,0.00009082287,0.0003512748,0.0006442416,0.0002141517],"domain_scores_gemma":[0.997965,0.0008437543,0.00006847062,0.0007023153,0.0003525223,0.00006791413],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.00006265575,0.00006756475,0.0004723796,0.0002563611,0.00003360175,0.0003694094,0.001361419,0.00456003,0.008989019,0.9182832,0.004783268,0.06076108],"study_design_scores_gemma":[0.0001187797,0.0000672499,0.001731878,0.0001579527,0.00006580304,0.00071172,0.0003158846,0.03809668,0.03273222,0.7769912,0.1489177,0.00009291893],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"other","genre_scores_codex":[0.03398754,0.000661651,0.9163123,0.002955144,0.000346483,0.000222668,0.0006572686,0.005198271,0.03965874],"genre_scores_gemma":[0.513176,0.0007072354,0.4702206,0.0005841911,0.0001686551,0.0001632654,0.000651793,0.0009579792,0.0133703],"genre_candidate":"other","genre_consensus":null,"teacher_disagreement_score":0.006966959,"threshold_uncertainty_score":0.02330679,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.09279825948958403,"score_gpt":0.1724514126866458,"score_spread":0.07965315319706176,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}