{"id":"W1814275833","doi":"10.1007/978-3-642-14052-5_27","title":"On the Formalization of the Lebesgue Integration Theory in HOL","year":2010,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Logic, Reasoning, and Knowledge","field":"Computer Science","cited_by":75,"is_retracted":false,"has_abstract":false,"ca_institutions":"Concordia University","funders":"","keywords":"Lebesgue integration; Mathematics; Discrete mathematics; Algebra over a field; Pure mathematics","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.001708346,0.0002962923,0.0002644793,0.0003502046,0.0002370658,0.0002175348,0.003520539,0.0002799342,0.00001993972],"category_scores_gemma":[0.0004567252,0.0001543626,0.0001137401,0.0006423742,0.0007413752,0.0003425003,0.0007844903,0.001005339,0.00001331532],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001198044,"about_ca_system_score_gemma":0.0003254257,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001807851,"about_ca_topic_score_gemma":0.0004645749,"domain_scores_codex":[0.9979433,0.0001050736,0.0003776498,0.0006340645,0.0006201983,0.000319663],"domain_scores_gemma":[0.9972179,0.0009644567,0.0003152608,0.001271567,0.0001899836,0.0000408323],"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.000004402136,0.00002245037,0.00005339805,0.000008715941,0.000002303529,0.000002315617,0.00218238,0.002532484,0.0003654475,0.8351406,0.000009847372,0.1596756],"study_design_scores_gemma":[0.000128895,0.0000994233,0.0006084453,0.0003706591,0.000003728919,0.00001348287,6.580873e-7,0.1683828,0.01421964,0.8155906,0.0003280063,0.0002537098],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.0008897542,0.00009724068,0.9832696,0.0006274686,0.001727945,0.0004282919,0.000001462639,0.00003545912,0.01292282],"genre_scores_gemma":[0.9840466,0.00001640189,0.01407031,0.00126679,0.0001845304,0.00001159157,0.000001746576,0.00001541738,0.0003866218],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.9831569,"threshold_uncertainty_score":0.6542097,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01240906446906039,"score_gpt":0.2241418883832711,"score_spread":0.2117328239142107,"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."}}